Completion-Based Automated Theory Exploration

Completion-based automated theory exploration is a method to explore inductive theories with the aid of a convergent rewrite system. It combines a method to synthesise conjectures/definitions in a theory with a completion algorithm. Completion constructs a convergent rewrite system which is then used to reduce redundancies and improve prove automation during the exploration of the theory. However, completion does not always succeed on a set of identities and a reduction ordering. A common failure occurs when an initial identity or a normal form of a critical pair cannot be oriented by the given ordering. A popular solution to this problem consists in using the instances of those rules which can be oriented for rewriting, namely ordered rewriting. Extending completion to ordered rewriting leads to ‘unfailing completion’. In this paper, we extend the class of theories on which the completion-based automated theory exploration method can be applied by using unfailing completion. This produce stronger normalization methods compared to those in [20,21]. The techniques described are implemented in the theory exploration system IsaScheme.