Mathematical applications of inductive logic programming

• Published in: Machine learning 2006-09, Vol.64 (1-3), p.25-64
• Main Authors: COLTON, Simon, MUGGLETON, Stephen
• Format: Article
• Language: English
• Subjects: Applied sciences; Artificial intelligence; Computer science; control theory; systems; Exact sciences and technology; Logic and foundations; Logic programming; Mathematical logic, foundations, set theory; Mathematics; Problem solving, game playing; Sciences and techniques of general use
• ISSN: 0885-6125; 1573-0565
• DOI: 10.1007/s10994-006-8259-x

Issue Title: Special ILP Mega-Issue: ILP-2003 and ILP-2004; ILP-2003 Guest Editors: Tamás Horváth and Akihiro Yamamoto; ILP-2004 Guest Editors: Rui Camacho, Ross King and Ashwin Srinivasan 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 of HR 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 importan