E-Generalization Using Grammars
This work addresses the problem of generalization under equational constraints for researchers in automated reasoning and inductive learning, representing an incremental extension of existing anti-unification methods.
The authors tackled the problem of extending anti-unification to equational theories by developing a method using regular tree grammars to compute finite representations of E-generalization sets, resulting in a framework that integrates Inductive Logic Programming and E-generalization, with applications demonstrated in lemma suggestion, term sequence construction, and command sequence learning.
We extend the notion of anti-unification to cover equational theories and present a method based on regular tree grammars to compute a finite representation of E-generalization sets. We present a framework to combine Inductive Logic Programming and E-generalization that includes an extension of Plotkin's lgg theorem to the equational case. We demonstrate the potential power of E-generalization by three example applications: computation of suggestions for auxiliary lemmas in equational inductive proofs, computation of construction laws for given term sequences, and learning of screen editor command sequences.