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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-89-14_Gramlich_Inductive-Theorem_Proving-Using-Refined-Unfailing-Completion-Techniques.pdf | 32,75 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.