Automata-Driven Automated Induction
This work extends refutationally complete explicit induction
techniques to partial functions whose meaning and domains can both be
specified by Horn Clauses built up from the equality and membership
predicates. In contrast with other works in the area, constructors are
not assumed to be free. Techniques originating from tree automata are
used to describe ground constructor terms in normal form, on which the
induction proofs are built up. Validity of constructor clauses is
checked by an original technique relying on the recent discovery by
Comon and delor of a complete axiomatisation of finite trees and their
rational subsets. Validity of clauses with defined symbols is reduced
to the latter case by appropriate inference rules using a notion of
ground reducibility for these symbols. We show how to check this
property by adapting usual techniques.
full paper