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