Theorem Proving in Hierarchical Clausal Specifications Juergen Avenhaus, Klaus Maldener Fachbereich Informatik, Universitaet Kaiserslautern D-67663 Kaiserslautern, GERMANY E-mail: avenhaus@informatik.uni-kl.de 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 ${\cal 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 ${\cal 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. Source anonymous FTP server ftp.uni-kl.de [131.246.94.94] path: /reports_uni-kl/computer_science/SEKI/1995/ file: Avenhaus.SR-95-14.ps.gz