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