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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-96-05_Kerber-Sehn_Proving-Ground-Completeness-of-Resolution-by-Proof-Planning.pdf | 1,7 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.