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

Sofronie-Stokkermans, Viorica

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Journal Article

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

MPS-Authors

/persons/resource/persons45516

Sofronie-Stokkermans, Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2DF7-B

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.