Please use this identifier to cite or link to this item: doi:10.22028/D291-39824
Title: Construction of Equality Graphs
Author(s): Bläsius, Karl-Hans
Language: English
Year of Publication: 1986
Place of publication: Kaiserslautern
DDC notations: 004 Computer science, internet
Publikation type: Report
Abstract: The theoretical and practical problems of equality reasoning in Automated Deduction are notorious. A new method is presented to cope with the enormous search space that usually arises when equational axioms are present. Starting from an empty graph a production system constructs graphs which represent solutions for simpler problems defined by abstraction. These graphs contain global information and are plans for guiding the search for a proof of the original problem, represented in the final graph. The construction of equality graphs is based on the idea to search for the differences between two terms by seperating toplevel symbol and subterms of a functional term. The impact of the explicit representation of information contained in the inference system on the control of inferences is discussed. Finally the method is compared to other equality reasoning methods.
Link to this record: urn:nbn:de:bsz:291--ds-398241
Series name: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Series volume: 86,1
Date of registration: 31-Aug-2023
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professorship: SE - Sonstige
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
SEKI-REPORT-SR-86-01_Bläsius_Construction-of-Equality-Graphs.pdf9,86 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.