Learning from examples and counterexamples with equational background knowledge

The author presents a method to check whether an implicit representation (i.e., a formula of the form t/{t1,. . .,tn}, where t is viewed as a generalization of a set of examples and t1,. . .,tn are counterexamples) is a generalization with respect to a finite set of equations which describes the background knowledge problem; that is, whether there exists a ground (variable-free) instance of t which is not equivalent to any ground instance of t1,. . .,tn with respect to a set E of equations. Intuitively, the implicit representation t/{t 1,. . .,tn} is a generalization if the set of ground instances of the formula t/{t1,. . .,tn} is non-empty. Whereas this problem is in general undecidable since the equality is so, it is shown here that, in the case where the set E of equations is compiled into a ground convergent term rewriting system, one can easily discover concepts in theories described by a finite set of equations