Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40277
Titel: Inductive Theorem Proving Using Refined Unfailing Completion Techniques
VerfasserIn: Gramlich, Bernhard
Sprache: Englisch
Erscheinungsjahr: 1989
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: We present a brief overview on completion based inductive theorem proving techniques, point out the key concepts for the underlying "proof by consistency" - paradigm and isolate an abstract description of what is necessary for an algorithmic realization of such methods. In particular, we give several versions of proof orderings, which - under certain conditions - are well-suited for that purpose. Together with corresponding notions of (positive and negative) covering sets we get abstract "positive" and "negative" characterizations of inductive validity. As a consequence we can generalize known criteria for inductive validity, even for the cases where some of the conjectures may not be orientable or where the base system is terminating but not necessarily ground confluent. Furthermore we consider several refinements and optimizations of completion based inductive theorem proving techniques. In particular, sufficient criteria for being a covering set including restrictions of critical pairs (and the usage of non-equational inductive knowledge) are discussed. Moreover a couple of lemma generation methods are briefly summarized and classified. A new techniques of save generalization is particularly interesting, since it provides means for syntactic generalizations, i.e. simplifications, of conjectures without loosing semantic equivalence. Finally we present the main features and characteristics of UNICOM, an inductive theorem prover with refined unfailing completion techniques and built on top of TRSPEC, a term rewriting based system for investigating algebraic specifications.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-402779
hdl:20.500.11880/36213
http://dx.doi.org/10.22028/D291-40277
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 89,14
Datum des Eintrags: 11-Aug-2023
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-89-14_Gramlich_Inductive-Theorem_Proving-Using-Refined-Unfailing-Completion-Techniques.pdf32,75 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.