Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41438
Titel: The New Standard Tactics of the Inductive Theorem Prover QUODLIBET
VerfasserIn: Schmidt-Samoa, Tobias
Sprache: Englisch
Erscheinungsjahr: 2004
Erscheinungsort: Saarbrücken
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: QUODLIBET is a tactic-based inductive theorem prover for the verification of algebraic specifications of algorithms in the style of abstract data types with positive/negative-conditional equations. Its core system consists of a small inference machine kernel that merely acts as a proof checker. Automation is achieved with tactics written in QML (QUODLIBET-Meta-Language), an adapted imperative programming language. In this paper, we describe QUODLIBET’s new standard tactics, a pool of general purpose tactics provided with the core system that support the user in proving inductive theorems. We aim at clarifying the underlying ideas as well as explaining the parameters with which the user can influence the behavior of the tactics during the proof process. One of the major achievements of this paper is the application of conditional lemmas controlled by obligatory and mandatory literals. This has drastically improved the degree of automation without increasing the runtime significantly as will be illustrated by the case studies. Nevertheless, the degree of automation depends on the specification style used. Thus, we will also give some guidelines how to write specifications and how to use the new tactics efficiently.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-414380
hdl:20.500.11880/37734
http://dx.doi.org/10.22028/D291-41438
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 2004,1
Datum des Eintrags: 28-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ößeFormat 
SEKI-Report-SR-2004-01_Schmidt=Samoa_The-New-Standard-Tactics-of-the-Inductive-Theorem-Prover-QUODLIBET.pdf55,58 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.