Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40261
Titel: Simplification and Reduction for Automated Theorem Proving
VerfasserIn: Socher-Ambrosius, Rolf
Sprache: Englisch
Erscheinungsjahr: 1990
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: The most severe obstacle on the way to the efficient automation of theorem proving is the size of the search space for drawing new inferences. There are two well known ways to overcome this difficulty. One solution comes under the term ”refutation strategies”, which denotes techniques to choose candidates for the next inference step. The other solution is termed ”reduction", which subsumes all techniques to remove those elements of the search space that do not contribute to the solution and thus are redundant. The second approach’s most critical part is the test on redundancy. Since each element of the search space has to be subjected to such a test, its efficiency is crucial for the value of the reduction approach. Subsumption, being one of the most important types of redundancy, is also a most problematic one. In this thesis, new and efficient tests for the variant and the subsumption property are developed, both based on the well known algorithms for detecting isomorphism of directed graphs. A most undesired aspect of redundancy is the derivation of subsumed clauses. Besides the problem with the subsumption test, the amount of computer time, which is spent for the derivation and normalization of such a clause, is purely wasted. In this thesis, the two approaches, strategy and reduction, are combined by a strategy to decrease the number of redundant information derived. This strategy is heavily based on a special treatment of logical equivalence. It turns out that this strategy represents a first step towards the answer of several open questions in automated theorem proving, like the problem with the derivation of redundant clauses, the choice of the appropriate representation and inference rule, the question for a theory to demodulate on the literal level, and finally the choice of clauses to apply a given inference rule. These problems are discussed in Wos’ (1988) 33 Basic Research Problems.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-402616
hdl:20.500.11880/37664
http://dx.doi.org/10.22028/D291-40261
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 90,10
Datum des Eintrags: 17-Mai-2024
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-90-10_Socher=Ambrosius_Simplification-and-Reduction-for-Automated-Theorem-Proving.pdf7,51 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.