Automata-driven automated induction

This work investigates inductive theorem proving techniques for first-order functions whose meaning and domains can be specified by Horn clauses built up from the equality and finitely many unary membership predicates. In con trast with other works in the area, constructors are not assumed to be free . Techniques originating from tree automata are used to describe ground con structor terms in normal form, on which the induction proofs are built up. Validity of (free) constructor clauses is checked by an original technique relying on the recent discovery of a complete axiomatization of finite tree s and their rational subsets. Validity of clauses with defined symbols or n onfree constructor terms is reduced to the latter case by appropriate infer ence rules using a notion of ground reducibility for these symbols. We show how to check this property by generating proof obligations which can be pa ssed over to the inductive prover. (C) 2001 Academic Press.