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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-93-01_Fuchs_Using-theorem-provers-for-PL1EQ-as-inductive-provers.pdf | 3,25 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.