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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-88-13_Müller-Socher-Ambrosius_Topics-in-Completion-Theorem-Proving.pdf | 15,97 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.