Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25718
Titel: Soft typing for clausal inference systems
Verfasser: Meyer, Christoph
Sprache: Englisch
Erscheinungsjahr: 1999
SWD-Schlagwörter: Automatisches Beweisverfahren ; Inferenzsystem ; Horn-Klausel ; Resolution <Logik> ; Gleichungstheorie ; Erfüllbarkeitsproblem
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: The purpose of this thesis is to study methods for the semantical control of automated theorem proving systems for first-order logic (with equality) based on certain effective abstraction techniques. We propose a general framework called soft typing for clausal inference systems to incorporate the validity/satisfiability of clauses with respect to certain model hypotheses into the control of inference systems. The effectiveness of the method is obtained by inferring automatically abstractions that result in approximations of validity/satisfiability of clauses with respect to these models. For an effective use of soft typing for ordered resolution and superposition, we propose the use of sets of Horn clauses (with equality) to represent approximations of model hypotheses for sets of clauses. We show that certain decidable fragments of first-order logic without equality can be generalized to non-trivial decidable equational theories. Our abstraction techniques, applied to arbitrary sets of clauses (with equality), result exactly in the decidable (equational) fragments. The satisfiability of clauses with respect to the approximations implies the satisfiability in the original model hypotheses.
Wir untersuchen Methoden zur semantischen Steuerung von automatischen Beweissystemen für Logik erster Stufe(mit Gleichheit) mit Hilfe von bestimmten berechenbaren Abstraktionstechniken. Wir schlagen ein allgemeines Konzept vor, das die Berücksichtigung der Gültigkeit beziehungsweise der Erfüllbarkeit von Klauseln bezüglich bestimmter Modellhypothesen in der Steuerung von Inferenzsystemen ermöglicht.Dieses Konzept nennen wir soft typing for clausal inference systems.Die Berechenbarkeit dieser Methoden wird durch automatische Abstraktionstechniken zur Approximation von Gültigkeit beziehungsweise von Erfüllbarkeit von Klauseln gewährleistet. Zur Darstellung der Approximationen von Modellhypothesen über Klauselmengen schlagen wir die Verwendung von Mengen von Hornklauseln (mit Gleichheit)vor, um Soft Typing von geordneter Resolution beziehungsweise Superposition zu ermöglichen. Wir zeigen, dass bestimmte entscheidbare Fragmente von Logik erster Stufe ohne Gleichheit zu nicht-trivialen entscheidbaren Gleichheitstheorien verallgemeinert werden können. Die Anwendung unserer Abstraktionstechniken auf beliebige Klauselmengen (mit Gleichheit) resultiert in diesen entscheidbaren Fragmenten (Gleichheitstheorien)wobei die Erfüllbarkeit von Klauseln bezüglich der Approximationen die Erfüllbarkeit in den ursprünglichen Modellhypothesen impliziert.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-2065
hdl:20.500.11880/25774
http://dx.doi.org/10.22028/D291-25718
Erstgutachter: Harald Ganzinger
Tag der mündlichen Prüfung: 5-Okt-1999
SciDok-Publikation: 29-Apr-2004
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
ChristophMeyerProfDrHaraldGanzinger.pdf1,49 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.