Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-24908
Titel: A resolution principle for clauses with constraints
Verfasser: Bürckert, Hans-Jürgen
Sprache: Englisch
Erscheinungsjahr: 1990
Quelle: Kaiserslautern ; Saarbrücken : DFKI, 1990
SWD-Schlagwörter: Künstliche Intelligenz
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: We introduce a general scheme for handling clauses whose variables are constrained by an underlying constraint theory. In general, constraints can be seen as quantifier restrictions as they filter out the values that can be assigned to the variables of a clause (or an arbitrary formulae with restricted universal or existential quantifier) in any of the models of the constraint theory. We present a resolution principle for clauses with constraints, where unification is replaced by testing constraints for satisfiability over the constraint theory. We show that this constrained resolution is sound and complete in that a set of clauses with constraints is unsatisfiable over the constraint theory if we can deduce a constrained empty clause for each model of the constraint theory, such that the empty clauses constraint is satisfiable in that model. We show also that we cannot require a better result in general, but we discuss certain tractable cases, where we need at most finitely many such empty clauses or even better only one of them as it is known in classical resolution, sorted resolution or resolution with theory unification.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-36690
hdl:20.500.11880/24964
http://dx.doi.org/10.22028/D291-24908
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Band: 90-02
SciDok-Publikation: 28-Jun-2011
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_90_02.pdf145,33 kBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.