Theorem Proving in Hierarchical Clausal Specifications

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.