SciDok

Eingang zum Volltext in SciDok

Lizenz

Report (Bericht) zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-50158
URL: http://scidok.sulb.uni-saarland.de/volltexte/2012/5015/


On skolemization in constrained logics

Bürckert, Hans-Jürgen ; Hollunder, Bernhard ; Laux, Armin

Quelle: (1993) Kaiserslautern ; Saarbrücken : DFKI, 1993
pdf-Format:
Dokument 1.pdf (5.621 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Künstliche Intelligenz
Institut: DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
DDC-Sachgruppe: Informatik
Dokumentart: Report (Bericht)
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Bandnummer: 93-06
Sprache: Englisch
Erstellungsjahr: 1993
Publikationsdatum: 05.12.2012
Kurzfassung auf Englisch: 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.
Lizenz: Standard-Veröffentlichungsvertrag

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English