Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40976
Titel: Integration of Rewriting, Narrowing, Compilation, and Heuristics for Equality Reasoning in Resolution-Based Theorem Proving
VerfasserIn: Präcklein, Axel
Sprache: Englisch
Erscheinungsjahr: 1992
Erscheinungsort: Saarbrücken
Freie Schlagwörter: Equality reasoning
Knuth-Bendix completion algorithm
Narrowing
Paramodulation
Resolution
Compilation
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: We present a framework for the integration of the Knuth-Bendix completion algorithm with narrowing methods, compiled rewrite rules, and a heuristic difference reduction mechanism for paramodulation. The possibility of embedding theory unification algorithms into this framework is outlined. Results are presented and discussed for several examples of equality reasoning problems in the context of an actual implementation of an automated theorem proving system (the MKRP-system) and a fast C implementation of the completion procedure. The MKRP-system is based on the clause graph resolution procedure. The thesis shows the indispensibility of the constraining effects of completion and rewriting for equality reasoning in general and quantifies the amount of speed-up caused by various enhancements of the basic method. The simplicity of the superposition inference rule allows to construct an abstract machine for completion, which is presented together with computation times for a concrete implementation.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-409766
hdl:20.500.11880/37668
http://dx.doi.org/10.22028/D291-40976
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 92,21
Datum des Eintrags: 21-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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.