Inductive Theorem Proving for Design Specifications

We present a number of new results on inductive theorem provingfor design specifications based on Horn logic with equality.Induction is explicit here because induction orderings aresupposed to be part of the specification. We show how the automatic support for program verification is enhanced if the specification satisfies a bunch of rewrite properties,summarized under the notion of canonicity. The enhancement isdue to inference rules and corresponding strategies whose soundness is implied by the specificationʹs canonicity. The second main result of the paper provides a method for proving canonicity by using the same rules, which are applied in proofs ofconjectures about the specification and the functional-logic programs it contains.