MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

MPI-I-2001-2-005

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

Sofronie-Stokkermans, Viorica

September 2001, 41 pages.

.
Status: available - back from printing

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.

  • MPI-I-2001-2-005.ps
  • Attachement: MPI-I-2001-2-005.ps (498 KBytes)

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2001-2-005

Hide details for BibTeXBibTeX
@TECHREPORT{Sofronie-Stokkermans2001,
  AUTHOR = {Sofronie-Stokkermans, Viorica},
  TITLE = {Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2001-2-005},
  MONTH = {September},
  YEAR = {2001},
  ISSN = {0946-011X},
}