Theorem Proving in Hierarchical Clausal Specifications

J. Avenhaus and K. Madlener
Additional contact information
J. Avenhaus: Universität Kaiserslautern, Fachbereich Informatik
K. Madlener: Universität Kaiserslautern, Fachbereich Informatik

A chapter in Advances in Algorithms, Languages, and Complexity, 1997, pp 1-51 from Springer

Abstract: Abstract In this paper we are interested in an algebraic specification language that (1) allows for sufficient expessiveness, (2) admits a well-defined se-mantics, 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 A spec 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 A spec. 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.

Keywords: Inference System; Inference Rule; Theorem Prove; Critical Pair; Ground Term (search for similar items in EconPapers)
Date: 1997
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4613-3394-4_1

Ordering information: This item can be ordered from
http://www.springer.com/9781461333944

DOI: 10.1007/978-1-4613-3394-4_1

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().