Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41424
Titel: Planning Mathematical Proofs with Methods
VerfasserIn: Huang, Xiaorong
Kerber, Manfred
Richts, Jörn
Sehn, Arthur
Sprache: Englisch
Erscheinungsjahr: 1994
Erscheinungsort: Saarbrücken
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: In this report we formally describe a declarative approach for encoding plan operators in proof planning, the so-called methods. The notion of method evolves from the much studied concept tactic and was first used by A. Bundy. Significant deductive power has been achieved with the planning approach towards automated deduction, however, the procedural character of the tactic part of methods hinders mechanical modification. Although the strength of a proof planning system largely depends on powerful general procedures which solve a large class of problems, mechanical or even automated modification of methods is nevertheless necessary for at least two reasons. Firstly methods designed for a specific type of problems will never be general enough. For instance, it is very difficult to encode a general method which solves all problems a human mathematician might intuitively consider as a case of homomorphy. Secondly the cognitive ability of adapting existing methods to suit novel situations is a fundamental part of human mathematical competence. We believe it is extremely valuable to computationally account for this kind of reasoning. The main part of this report is devoted to a declarative language for encoding methods, composed of a tactic and a specification. The major feature of our approach is that the tactic part of a method is split into a declarative and a procedural part in order to enable a tractable adaption of methods. The applicability of a method in a planning situation is formulated in the specification, essentially consisting of an object level formula schema and a meta-level formula of a declarative constraint language. After setting up our general framework, we mainly concentrate on this constraint language. Furthermore we illustrate how our methods can be used in a STRIPS-like planning framework. Finally we briefly show the mechanical modification of declaratively encoded methods. An annotated runtime protocol of an example can be found in the appendix.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-414241
hdl:20.500.11880/37732
http://dx.doi.org/10.22028/D291-41424
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 94,8
Datum des Eintrags: 28-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-94-08_Huang-Kerber-Richts-Sehn_Planning-Mathematical-Proofs-with-Methods.pdf2,91 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.