Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-25212
Titel: | On skolemization in constrained logics |
VerfasserIn: | Bürckert, Hans-Jürgen Hollunder, Bernhard Laux, Armin |
Sprache: | Englisch |
Erscheinungsjahr: | 1993 |
Quelle: | Kaiserslautern ; Saarbrücken : DFKI, 1993 |
Kontrollierte Schlagwörter: | Künstliche Intelligenz |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | 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 |
Datum des Eintrags: | 5-Dez-2012 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
RR_93_06_.pdf | 5,62 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.