×

Mathematical applications of inductive logic programming. (English) Zbl 1103.68438

Summary: 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 ILP for mathematical discovery [Proc Thirteenth International Conference on Inductive Programming, S. 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 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.

MSC:

68N17 Logic programming
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abell, M., & Braselton, J. (1994). Maple V by example. Associated Press Professional. · Zbl 0799.65001
[2] Brachman, R., & Levesque, H. (Eds.), (1985). Readings in knowledge representation. Morgan Kaufmann. · Zbl 0609.68007
[3] Caporossi, G., & Hansen, P. (1999), Finding relations in polynomial time. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence.
[4] Colton, S. (1999). Refactorable numbers–a machine invention. Journal of Integer Sequences, 2. · Zbl 1036.11540
[5] Colton, S. (2000). An application-based comparison of automated theory formation and inductive logic programming. Electronic Transactions in Artificial Intelligence, 4(B).
[6] Colton, S. (2002a). Automated theory formation applied to mutagenesis data. In: Proceedings of the First British-Cuban Workshop on BioInformatics.
[7] Colton, S. (2002b). Automated theory formation in pure mathematics. Springer-Verlag. · Zbl 1219.68141
[8] Colton, S. (2002c). The HR program for theorem generation. In: Proceedings of the Eighteenth Conference on Automated Deduction. · Zbl 1072.68567
[9] Colton, S. (2002d). Making conjectures about maple functions. In: Proceedings of the Tenth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, LNAI 2385. Springer-Verlag. · Zbl 1072.68656
[10] Colton, S. (2003). ILP for mathematical discovery In: Proceedings of the Thirteenth International Conference on Inductive Logic Programming. · Zbl 1263.68127
[11] Colton, S., Bundy, A., & Walsh, T. (2000a). Automatic identification of mathematical concepts. In: Machine Learning: Proceedings of the Seventeenth International Conference. · Zbl 1011.68621
[12] Colton, S., Bundy, A., & Walsh, T. (2000b). Automatic invention of integer sequences. In: Proceedings of the Seventeenth National Conference on Artificial Intelligence. · Zbl 1011.68621
[13] Colton, S., Bundy, A., & Walsh, T. (2000c). On the notion of interestingness in automated mathematical discovery. International Journal of Human Computer Studies, 53(3), 351–375. · Zbl 1011.68621
[14] Colton, S., & Dennis, L. (2002). The NumbersWithNames Program. In: Proceedings of the Seventh AI and Maths Symposium.
[15] Colton, S., & Huczynska, S. (2003). The HOMER system. In: Proceedings of the Nineteenth International Conference on Automated Deduction (LNAI 2741). (pp. 289–294). · Zbl 1214.68332
[16] Colton, S., Meier, A., Sorge, V., & McCasland, R. (2004). Automatic generation of classification theorems for finite algebras. In: Proceedings of the International Joint Conference on Automated Reasoning. · Zbl 1126.68562
[17] Colton, S., Miguel, I. (2001). Constraint generation via automated theory formation. In: Proceedings of CP-01. · Zbl 1067.68622
[18] Colton, S., Pease, A. (2003). Lakatos-style methods in automated reasoning. In: Proceedings of the IJCAI’03 Workshop on Agents and Reasoning.
[19] Colton, S., & Pease, A. (2004). The TM system for repairing non-theorems. In: Proceedings of the IJCAR’04 Disproving Workshop. · Zbl 1272.68352
[20] Colton, S., & Sutcliffe, G. (2002). Automatic generation of benchmark problems for automated theorem proving systems. In: Proceedings of the Seventh AI and Maths Symposium.
[21] Conway, J. (1976). On numbers and games. Academic Press. · Zbl 0334.00004
[22] De Raedt, L., & Dehaspe, L. (1997). Clausal discovery. Machine Learning, 26, 99–146. · Zbl 0866.68021
[23] Dehaspe, L., & Toivonen, H. (1999). Discovery of frequent datalog patterns. Data Mining and Knowledge Discovery, 3(1), 7–36. · Zbl 05468033
[24] Epstein, S. (1988). Learning and discovery: One system’s search for mathematical knowledge. Computational Intelligence, 4(1), 42–53.
[25] Fajtlowicz, S. (1988). On conjectures of Graffiti. Discrete Mathematics, 72, (23), 113–118. · Zbl 0711.68081
[26] Franke, A., & Kohlhase, M. (1999). System description: MATHWEB, an agent-based communication layer for distributed automated theorem proving. In: Proceedings of the Sixteenth Conference on Automated Deduction. (pp. 217–221).
[27] Gap (2000). GAP reference manual. The GAP Group, School of Mathematical and Computational Sciences, University of St. Andrews.
[28] Humphreys, J. (1996). A Course in group theory. Oxford University Press. · Zbl 0843.20001
[29] Jackson, P. (1992). Computing prime implicates incrementally. In: Proceedings of CADE 11. · Zbl 0925.03054
[30] Lakatos, I. (1976). Proofs and refutations: The logic of mathematical discovery. Cambridge University Press. · Zbl 0334.00022
[31] Lenat, D. (1982). AM: discovery in mathematics as heuristic search. In: D. Lenat and R. Davis (Eds.), Knowledge-based systems in artificial intelligence. McGraw-Hill Advanced Computer Science Series. · Zbl 0479.68093
[32] McCune, W. (1990). The OTTER user’s guide. Technical Report ANL/90/9, Argonne National Laboratories.
[33] McCune, W. (1994). A Davis-Putnam program and its application to finite first-order model search. Technical Report ANL/MCS-TM-194, Argonne National Laboratories.
[34] Meier, A., Sorge, V., & Colton, S. (2002). Employing theory formation to guide proof planning. In: Proceedings of the Tenth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, LNAI 2385. Springer-Verlag. · Zbl 1072.68582
[35] Mohamadali, N. (2003). A Rational reconstruction of the graffiti program. Master’s thesis, Department of Computing, Imperial College, London.
[36] Muggleton, S. (1995). Inverse entailment and Progol. New Generation Computing, 13, 245–286. · Zbl 05479869
[37] Quinlan, R. (1993). C4.5: Programs for machine learning. Morgan Kaufmann.
[38] Sims, M., & Bresina, J. (1989). Discovering mathematical operator definitions. In: Machine Learning: Proceedings of the Sixth International Conference. Morgan Kaufmann.
[39] Sloane, N. (2000). The online Encyclopedia of Integer Sequences. http://www.research.att.com/\(\sim\)njas/sequences
[40] Srinivasan, A., Muggleton, S., King, R., & Sternberg, M. (1996). Theories for mutagenicity: A study of first-order and feature based induction’. Artificial Intelligence, 85(1, 2), 277–299.
[41] Steel, G. (1999). Cross domain concept formation using HR. Master’s thesis, Division of Informatics, University of Edinburgh.
[42] Sutcliffe, G., & Suttner, C. (1998). The TPTP problem library: CNF release v1.2.1’. Journal of Automated Reasoning, 21(2), 177–203. · Zbl 0910.68197
[43] Weidenbach, C. (1999). SPASS: Combining superposition, sorts and splitting. In: R. A and V. A (Eds.), Handbook of automated reasoning. Elsevier Science.
[44] Zimmer, J., Franke, A., Colton, S., & Sutcliffe, G. (2002). Integrating HR and tptp2x into MathWeb to compare automated theorem provers. In: Proceedings of the CADE’02 Workshop on Problems and Problem sets.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.