Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25212
Titel: On skolemization in constrained logics
Verfasser: Bürckert, Hans-Jürgen
Hollunder, Bernhard
Laux, Armin
Sprache: Englisch
Erscheinungsjahr: 1993
Quelle: Kaiserslautern ; Saarbrücken : DFKI, 1993
SWD-Schlagwörter: Künstliche Intelligenz
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: First-order logics allows one to quantify over all elements of the universe. However, it is often more natural to quantify only over those elements which satisfy a certain condition. Constrained logics provide this possibility by introducing restricted quantifiers ∀ X:R F and ∃ X:R F where X is a set of variables, and which can be read as "F holds for all elements satisfy R", respectively. In order to test unsatisfiability of a set of such formulas using an extended resolution principle, one needs a procedure which transforms them into a set of constrained clauses. Such a procedure causes more problems than the classical transformation of first-order formulas into a set of clauses. This is due to the fact that quantification over the empty set may occur. Especially, a modified Skolemization procedure has to be used in order to remove restricted existential quantifiers. In this paper we will give a procedure that transforms formulas with restricted quantifiers into a set of clauses with constraints preserving unsatisfiability. Since restrictions may be given by sorts this procedure can, e.g., be applied to sorted logics where empty sorts may occur. The obtained clauses are of the form C || R where C is an ordinary clause and R is a restriction, and which can be read as "C holds if R holds". They can be tested on unsatisfiability via constrained resolution. Finally, we introduce so-called constraint unification which can be used for optimization of constrained resolution if certain conditions are satisfied.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-50158
hdl:20.500.11880/25268
http://dx.doi.org/10.22028/D291-25212
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Band: 93-06
SciDok-Publikation: 5-Dez-2012
Fakultät: Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Fakultät / Institution:SE - Sonstige Einrichtungen

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
RR_93_06_.pdf5,62 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.