Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-39690
Titel: Topics in Completion Theorem Proving
VerfasserIn: Müller, Jürgen
Socher-Ambrosius, Rolf
Sprache: Englisch
Erscheinungsjahr: 1988
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: Completion Theorem Proving is based on the observation that proving a formula is equivalent to solving a system of equations over a boolean polynomial ring. The latter can be accomplished by means of the completion of a set of rewrite rules Obtained from the equational system. This report deals with three problems concerning Completion Theorem Provers (CTPs): - Are multiple overlaps necessary for the completeness of CTPs? - How can simplification be interpreted in terms of resolution inference rules ? - How can polynomials efficiently be represented? The answer to the first question is “no”. Even more it is shown in this report that the removal of multiple overlap steps does not increase the length of completion refutations. This amounts to an extension of Dietrich’s (1986) result concerning the correspondence of completion proofs without simplification for Horn Logic to resolution proofs. Concerning the second question we show that simplification in general cannot be translated into resolution reduction rules. However, two special cases of reduction can be interpreted as subsumption deletion and replacement resolution, respectively. Changing the point of view, we can also identify resolution reduction rules, such as tautology elimination, merging and subsumption deletion, as part of CTPs without being explicitly defined as inference rules. The last section deals with the technical question of choosing a datastructure well suited for an efficient implementation of CTPs.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-396900
hdl:20.500.11880/36028
http://dx.doi.org/10.22028/D291-39690
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 88,13
Datum des Eintrags: 22-Jun-2023
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professur: SE - Sonstige
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
SEKI-Report-SR-88-13_Müller-Socher-Ambrosius_Topics-in-Completion-Theorem-Proving.pdf15,97 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.