Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40429
Titel: | Completion Based Inductive Theorem Proving : A Case Study in Verifying Sorting Algorithms |
VerfasserIn: | Gramlich, Bernhard |
Sprache: | Englisch |
Erscheinungsjahr: | 1990 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | The focus of this paper lies on practical aspects of completion based inductive theorem proving in equational theories. As domain of interest we concentrate on the mechanically supported verification of a couple of sorting algorithms. The experiments have been performed with UNICOM, an inductive theorem prover based on refined unfailing completion techniques. We summarize these experiments, point out important technical and conceptual aspects and illustrate them by numerous examples. In particular we discuss and exemplify the kind of intelligent proof engineering required for succeeding in non-trivial verification problems. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-404292 hdl:20.500.11880/37652 http://dx.doi.org/10.22028/D291-40429 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 90,4 |
Datum des Eintrags: | 16-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öße | Format | |
---|---|---|---|---|
SEKI_Report-SR-90-04_Gramlich_Completion-Based-Inductive-Theorem-Proving=A-Case-Study-in-Verifying-Sorting-Algorithms.pdf | 31,44 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.