Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41486
Titel: Theorem Proving in Hierarchical Clausal Specifications
VerfasserIn: Avenhaus, Jürgen
Maldener, Klaus
Sprache: Englisch
Erscheinungsjahr: 1995
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: In this paper we are interested in an algebraic specification language that (1) allows for sufficient expessiveness, (2) admits a well-defined semantics, and (3) allows for formal proofs. To that end we study clausal specifications over built-in algebras. To keep things simple, we consider built-in algebras only that are given as the initial model of a Horn clause specification. On top of this Horn clause specification new operators are (partially) defined by positive/negative conditional equations. In the first part of the paper we define three types of semantics for such a hierarchical specification: model-theoretic, operational, and rewrite-based semantics. We show that all these semantics coincide, provided some restrictions are met. We associate a distinguished algebra Aspec to a hierachical specification spec. This algebra is initial in the class of all models of spec. In the second part of the paper we study how to prove a theorem (a clause) valid in the distinguished algebra Aspec. We first present an abstract framework for inductive theorem provers. Then we instantiate this framework for proving inductive validity. Finally we give some examples to show how concrete proofs are carried out.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-414867
hdl:20.500.11880/37783
http://dx.doi.org/10.22028/D291-41486
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 95,14
Datum des Eintrags: 4-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-95-14_Avenhaus-Maldener_Theorem-Proving-in-Hierarchical-Clausal-Specifications .pdf4,01 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.