Treffer: Mathematical applications of inductive logic programming

The application of Inductive Logic Programming to scientific datasets has been highly successful. Such applications have led to breakthroughs in the domain of interest and have driven the development of ILP systems. The application of AI techniques to mathematical discovery tasks, however, has largely involved computer algebra systems and theorem provers rather than machine learning systems. We discuss here the application of the HR and Progol machine learning programs to discovery tasks in mathematics. While Progol is an established ILP system, HR has historically not been described as an ILP system. However, many applications of HR have required the production of first order hypotheses given data expressed in a Prolog-style manner, and the core functionality of HR can be expressed in ILP terminology. In Colton (2003), we presented the first partial description of HR as an ILP system, and we build on this work to provide a full description here. HR performs a novel ILP routine called Automated Theory Formation, which combines inductive and deductive reasoning to form clausal theories consisting of classification rules and association rules. HR generates definitions using a set of production rules, interprets the definitions as classification rules, then uses the success sets of the definitions to induce hypotheses from which it extracts association rules. It uses third party theorem provers and model generators to check whether the association rules are entailed by a set of user supplied axioms. HR has been applied successfully to a number of predictive, descriptive and subgroup discovery tasks in domains of pure mathematics. We survey various applications ofHR which have led to it producing number theory results worthy of journal publication, graph theory results rivalling those of the highly successful Graffiti program and algebraic results leading to novel classification theorems. To further promote mathematics as a challenge domain for ILP systems, we present the first application of Progol to an algebraic domain-we use Progol to find algebraic properties of quasigroups, semigroups and magmas (groupoids) of varying sizes which differentiate pairs of non-isomorphic objects. This development is particularly interesting because algebraic domains have been an important proving ground for both deduction systems and constraint solvers. We believe that AI programs written for discovery tasks will need to simultaneously employ a variety of reasoning techniques such as induction, abduction, deduction, calculation and invention. We argue that mathematics is not only a challenging domain for the application of ILP systems, but that mathematics could be a good domain in which to develop a new generation of systems which integrate various reasoning techniques.