Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40258
Titel: Solving Equality Reasoning Problems with a Connection Graph Theorem Prover
VerfasserIn: Präcklein, Axel
Sprache: Englisch
Erscheinungsjahr: 1990
Erscheinungsort: Kaiserslautern
Freie Schlagwörter: Equality reasoning
Knuth-Bendix algorithm
paramodulation
resolution
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: The integration of a Knuth-Bendix completion algorithm into a paramodulation theorem prover on the basis of a connection graph resolution procedure is presented. The Knuth-Bendix completion idea is compared to a decomposition approach, and some ideas to handle conditional equations are discussed. The contents of this paper is not intended to present new material on term rewriting, instead it is more a pleading for the usage of completion ideas in automated deduction. It records our experience with an actual implementation of a hybrid system, where a completion procedure was imbedded into a connection graph theorem prover, the MKRP-system, with satisfactory positive results.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-402585
hdl:20.500.11880/36265
http://dx.doi.org/10.22028/D291-40258
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 90,7
Datum des Eintrags: 14-Aug-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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.