Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41009
Titel: Using theorem provers for PL1EQ as inductive provers
VerfasserIn: Fuchs, Matthias
Sprache: Englisch
Erscheinungsjahr: 1992
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: This report presents a method to create an inductive proof system by using a theorem prover for PL1EQ (first order logic with equality) as a basic system. This method not only comprises the general principles necessary for making a theorem prover for PL1EQ capable of performing inductive proofs, but also includes further features that may be added to systems for inductive proofs in order to guide the individual proof (for instance heuristics aimed at optimizing the application of the inference rules with respect to the fact that a proof by induction is to be found). An emphasis lies on the automatic generation of inductive Iemmata which are crucial to the success of inductive proofs. In this domain a range of heuristics were conceived, partly as derivations of ideas of other authors, partly as own developments, which in many cases can generate a lemma that ends the proof attempt successfully. (This includes that this lemma itself can be proved by induction as well.)
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-410094
hdl:20.500.11880/37794
http://dx.doi.org/10.22028/D291-41009
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 93,1
Datum des Eintrags: 5-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ößeFormat 
SEKI-Report-SR-93-01_Fuchs_Using-theorem-provers-for-PL1EQ-as-inductive-provers.pdf3,25 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.