Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40773
Titel: Towards Intelligent Inductive Proof Engineering
VerfasserIn: Gramlich, Bernhard
Sprache: Englisch
Erscheinungsjahr: 1992
Erscheinungsort: Kaiserslautern
Freie Schlagwörter: inductive theorem proving
proof engineering
term rewriting
completion
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: This paper deals with inductive theorem proving (ITP for short). It does not provide new theoretical results but analyses existing ITP methods from an AI point of view. The presentation is based on the implicit ITP approach, i.e. ITP using the well-developed framework of rewriting and completion techniques for systems of equations and rewrite rules. We think that the relevant practical problems for successful (partially) automated ITP are essentially the same as or at least closely related to those occurring in the more conventional framework of explicit ITP using schemas. The theoretical foundations of implicit ITP are briefly reviewed focussing on the central ideas as well as on important operationalization issues. Moreover, a brief comparison of explicit and implicit ITP approaches is included. In particular, we clarify some criticisms raised against the implicit ITP approach. The main part of the paper is devoted to a thorough discussion of central ITP problems from the viewpoint of system designers and users. We point out and exemplify the necessity of linking together the whole process of formalizing, modelling and structuring abstract (equational) specifications of algorithms and corresponding (inductive) properties to be verified. Crucial aspects of the whole specification and proof engineering process are isolated and discussed, in particular conceptual and proof-technical ones. We argue that such an analysis (which of course has to be continued and deepened) is necessary for an adequate integration and combination of intelligent user-guided and machine-supported automated inductive reasoning. Finally the main theoretical and practical problems as well as promising perspectives for future work are sketched, in particular concerning architectural and design principles for future generation inductive theorem provers.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-407738
hdl:20.500.11880/37672
http://dx.doi.org/10.22028/D291-40773
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 92,1
Datum des Eintrags: 21-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-92-01_Gramlich_Towards-Intelligent-Inductive-Proof-Engineering.pdf1,94 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.