Please use this identifier to cite or link to this item: doi:10.22028/D291-41486
Title: Theorem Proving in Hierarchical Clausal Specifications
Author(s): Avenhaus, Jürgen
Maldener, Klaus
Language: English
Year of Publication: 1995
Place of publication: Kaiserslautern
DDC notations: 004 Computer science, internet
Publikation type: Report
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 to this record: urn:nbn:de:bsz:291--ds-414867
Series name: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Series volume: 95,14
Date of registration: 4-Jun-2024
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professorship: SE - Sonstige
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.