Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41578
Titel: Proving Ground Completeness of Resolution by Proof Planning
VerfasserIn: Kerber, Manfred
Sehn, Arthur Christian
Sprache: Englisch
Erscheinungsjahr: 1996
Erscheinungsort: Saarbrücken
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: A lot of the human ability to prove hard mathematical theorems can be ascribed to a problem-specific problem solving know-how. Such knowledge is intrinsically incomplete. In order to prove related problems human mathematicians, however, can go beyond the acquired knowledge by adapting their know-how to new related problems. These two aspects, having rich experience and extending it by need, can be simulated in a proof planning framework: the problem-specific reasoning knowledge is represented in form of declarative planning operators, called methods; since these are declarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs in theorem proving, first, we present methods for proving the ground completeness of binary resolution, which essentially correspond to key lemmata, and then, we show how these methods can be reused for the proof of the ground completeness of lock resolution.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-415786
hdl:20.500.11880/37811
http://dx.doi.org/10.22028/D291-41578
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 96,5
Datum des Eintrags: 6-Jun-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-96-05_Kerber-Sehn_Proving-Ground-Completeness-of-Resolution-by-Proof-Planning.pdf1,7 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.