English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators

Sofronie-Stokkermans, V. (2003). Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators. Journal of Symbolic Computation, 36, 891-924.

Item is

Files

show Files
hide Files
:
jsc-2003.pdf (Publisher version), 398KB
 
File Permalink:
-
Name:
jsc-2003.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
Copyright Elsevier Publishers
License:
-

Locators

show

Creators

show
hide
 Creators:
Sofronie-Stokkermans, Viorica1, 2, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We establish a link between the satisfiability of universal sentences with respect to classes of distributive lattices with operators and their satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal theory of some such classes. In particular, we obtain exponential space and time decision procedures for the universal clause theory of (i) the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, (ii) the class of all bounded distributive lattices with operators, and a doubly-exponential time decision procedure for the universal clause theory of the class of all Heyting algebras.

Details

show
hide
Language(s): eng - English
 Dates: 2004-06-172003
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: eDoc: 201909
Other: Local-ID: C1256104005ECAFC-CEC92761F334BFFAC1256CB50050C081-Sofronie-Stokkermans-jsc-2003
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Journal of Symbolic Computation
Source Genre: Journal
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 36 Sequence Number: - Start / End Page: 891 - 924 Identifier: ISSN: 0747-7171