Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41395
Titel: Guiding Equational Proofs by Attribute Functions
VerfasserIn: Cleve, Jürgen
Hutter, Dieter
Sprache: Englisch
Erscheinungsjahr: 1993
Erscheinungsort: Saarbrücken
Freie Schlagwörter: Deduction
Automated Reasoning
Equational Reasoning
Difference Reduction
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: This report presents a methodology to guide equational reasoning in a goal directed way. Suggested by rippling methods developed in the field of inductive theorem proving we use attributes of terms and heuristics to determine bridge lemmas, i.e. lemmas which have to be used during the proof of the theorem. Once we have found such a bridge lemma we use the techniques of difference unification and rippling to enable its use.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-413952
hdl:20.500.11880/37711
http://dx.doi.org/10.22028/D291-41395
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 93,15
Datum des Eintrags: 27-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-93-15_Cleve-Hutter_Guiding-Equational-Proofs-by-Attribute-Functions .pdf1,57 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.