Stuber, Jürgen

Inductive Theorem Proving for {H}orn Clauses

We show how to prove inductive consequences of horn clause
specifications by horn clause completion. Most often one is
interested in properties of the initial algebra. These stem from the
facts that (a) it is generated by ground terms, and that (b) only
provable ground equations are valid in the initial algebra. (a) is
the basis of proofs by structural induction. (b) becomes relevant in
the case of horn clauses, since the validity of a horn clause may
depend on the fact that the conditions do not become true too often.
We show that (a) is true for term generated algebras, whereas (b) is
true for free algebras. Sophisticated completion procedures for horn
clauses already carry out inductive proofs of type (b), in order to