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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.