Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  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

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2DF7-B Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2DF8-9
Genre: Zeitschriftenartikel

Dateien

einblenden: Dateien
ausblenden: Dateien
:
jsc-2003.pdf (Verlagsversion), 398KB
 
Datei-Permalink:
-
Name:
jsc-2003.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/pdf
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
Copyright Elsevier Publishers
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Sofronie-Stokkermans, Viorica1, 2, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2004-06-172003
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: Expertenbegutachtung
 Identifikatoren: eDoc: 201909
Anderer: Local-ID: C1256104005ECAFC-CEC92761F334BFFAC1256CB50050C081-Sofronie-Stokkermans-jsc-2003
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Journal of Symbolic Computation
Genre der Quelle: Zeitschrift
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 36 Artikelnummer: - Start- / Endseite: 891 - 924 Identifikator: ISSN: 0747-7171