Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41608
Titel: An Abstraction for Proof Planning : The S-Abstraction
VerfasserIn: Autexier, Serge
Sprache: Englisch
Erscheinungsjahr: 1997
Erscheinungsort: Saarbrücken
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: This paper presents a new kind of abstraction, which has been developed for the purpose of proof planning. The basic idea of this paper is to abstract a given theorem and to find an abstract proof of it. Once an abstract proof has been found, this proof has to be refined to a real proof of the original theorem. We present a goal oriented abstraction for the purpose of equality proof planning, which is parameterized by common parts of the left- and right-hand sides of the given equality. Therefore, this abstraction technique provides an abstract equality problem which is more adequate than those generated by the abstractions known so far. The presented abstraction also supports the heuristic search process based on the difference reduction paradigm. We give a formal definition of the abstract space including the objects and their manipulation. Furthermore, we prove some properties in order to allow an efficient implementation of the presented abstraction.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-416084
hdl:20.500.11880/37826
http://dx.doi.org/10.22028/D291-41608
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 97,5
Datum des Eintrags: 7-Jun-2024
Bemerkung/Hinweis: Seiten 5 und 6 nicht vorhanden.
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-97-05_Autexier_An-Abstraction-for-Proof-Planning-The-S=Abstraction.pdf2,53 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.