max planck institut
informatik
informatik
MPI-I-2001-2-005. September 2001, 41 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
In this paper we establish a link between satisfiability of universal
sentences with respect to classes of distributive lattices with operators and
satisfiability with respect to certain classes of relational structures.
This justifies a method for structure-preserving translation to clause form
of universal (Horn) sentences in such classes of algebras.
We show that refinements of resolution yield decision procedures
for the universal (Horn) theory of some such classes.
In particular, we obtain exponential decision procedures
for the universal Horn theory of
(i) the class of all bounded distributive lattices with operators,
(ii) for the class of all bounded distributive lattices with operators
satisfying a set of (generalized) residuation conditions,
and a doubly-exponential decision procedure for the universal Horn theory of
the class of all Heyting algebras.
Acknowledgement:
References to related material:
| To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
|---|---|
| 498 KBytes | |
| Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView | |
BibTeX