Implementing Anti-Unification Modulo Equational Theory
This work provides a practical tool for automated reasoning and theorem proving, but it is incremental as it builds directly on prior theoretical definitions.
The authors implemented E-anti-unification as defined by Heinz (1995) to compute generalizations modulo equational theories, reporting runtime figures for efficiency improvements. They applied this to areas such as lemma generation in proofs and theory formation about finite algebras.
We present an implementation of E-anti-unification as defined in Heinz (1995), where tree-grammar descriptions of equivalence classes of terms are used to compute generalizations modulo equational theories. We discuss several improvements, including an efficient implementation of variable-restricted E-anti-unification from Heinz (1995), and give some runtime figures about them. We present applications in various areas, including lemma generation in equational inductive proofs, intelligence tests, diverging Knuth-Bendix completion, strengthening of induction hypotheses, and theory formation about finite algebras.