Generalization is an important operation for programs that learn. Anti-unification guarantees the existence of a term which is the most specific generalization of a collection of terms. This provides a formal basis for learning from examples. However, such generalization may be "too" general and therefore counterexamples are required to restrict them. In this case, the learner has to check whether the resulting formula provides a concept to learn, i.e. whether a formula of the form t/{t1,…,tn} is a generalization, where t is viewed as a generalization of a set of examples and t1,…,tn are counterexample. The formula t/{t1,…,tn} is often called an implicit representation. The implicit representation t/{t1,…,tn} is a generalization iff there exist ground (variable-free) instances of t which are not instances of t1,…,tn. This is a non-trivial task even when there is no background knowledge (see [15]). We present here a method to check whether an implicit representation t/{t1,…,tn} is a generalization with respect to a finite set of equations which describes the background knowledge problem, i.e. whether there exists a ground instance of t which is not equivalent to any ground instance of t1,…,tn with respect to a set E of equations. Whereas this problem is in general undecidable since the equality is so, we show in this paper that in this case where the set E of equations is compiled into a ground convergent term rewriting system, we can discover concepts in Universe of Discourse with background knowledge described by a finite set of equations. We show how the method applies to induce concepts in theories of elementary arithmetic.
HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA