Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Bericht

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

MPG-Autoren
/persons/resource/persons45516

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)

2001-2-005
(beliebiger Volltext), 11KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Sofronie-Stokkermans, V.(2001). Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators (MPI-I-2001-2-005). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-6CB3-4
Zusammenfassung
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.