HR – Automated Theory Formation

Research

Introduction

Automated Theory Formation (ATF) is a novel machine learning and discovery approach which has been developed over 15 years, and which is implemented in the HR systems (HR1 in Prolog, HR2 and HR3 in Java). Given some background knowledge, HR forms new concepts from old ones using a set of production rules, and then makes conjectures which relate the concepts, by appealing to empirical patterns in the examples of the concepts. HR then uses third party systems to prove/disprove the conjectures (usually the Otter theorem prover and the MACE model generator). HR also interacts with computer algebra systems such as Maple and Gap, in order to calculate values for concepts. To drive a heuristic search, HR uses a weighted sum – with the weights set by the user – of measures of interestingness for concepts, i.e., having decided which concept is most interesting, HR builds new concepts from this. The book arising from Simon Colton’s PhD work is the main reference text for the early work on Automated Theory Formation.

Talks

Here are three talks about the HR project, which give an overview of the project and different contexts for it:

The papers below describe how the HR systems have been developed, the applications to which they have been applied and a context in AI for the project.

Publications

The Development of Automated Theory Formation

The following papers describe some of the fundamental aspects of automated theory formation. The first paper is the main reference for ATF in the HR2 system, described as an Inductive Logic Programming system. The other papers are from quite early on in the development of ATF in the HR1 and HR2 systems.

Guckelsberger, Christian; Salge, Christoph; Gow, Jeremy; Cairns, Paul

Predicting Player Experience Without the Player. An Exploratory Study Inproceedings

In: Proc. ACM Symp. on Computer-Human Interaction in Play (CHIPlay’17), 2017.

Abstract | Links | BibTeX

Guckelsberger, Christian; Salge, Christoph; Colton, Simon

Addressing the "Why?" in Computational Creativity: A Non-Anthropocentric, Minimal Model of Intentional Creative Agency Inproceedings

In: Proc. 8th Int. Conf. Computational Creativity, 2017 , 2017.

Abstract | Links | BibTeX

Guckelsberger, Christian; Salge, Christoph; Colton, Simon

Intrinsically Motivated General Companion NPCs via Coupled Empowerment Maximisation Inproceedings

In: Proc. IEEE Conf. Computational Intelligence in Games (CIG’16), IEEE, 2016.

Abstract | Links | BibTeX

Guckelsberger, Christian; Salge, Christoph; Saunders, Rob; Colton, Simon

Supportive and Antagonistic Behaviour in Distributed Computational Creativity via Coupled Empowerment Maximisation Inproceedings

In: Proc. 7th Int. Conf. Computational Creativity, 2016.

Abstract | Links | BibTeX

Guckelsberger, Christian; Salge, Christoph

Does Empowerment Maximisation Allow for Enactive Artificial Agents? Inproceedings

In: Proc. 15th Int. Conf. Synthesis and Simulation of Living Systems (ALIFE), 2016.

Abstract | Links | BibTeX

More Sophisticated Mathematical Theory Formation Models

We have taken Automated Theory Formation as the basis for more in-depth studies into how mathematical theories can be formed automatically. In addition to providing extensions to the basic automated theory formation model and providing more background to the subject, these projects have led to more sophisticated systems for mathematical invention and machine learning in general, which take into account philosophical and psychological perspectives on theory formation. The following papers describe some of our projects in this area:

Schorlemmer, Marco; Smaill, Alan; Kühnberger, Kai-Uwe; Kutz, Oliver; Colton, Simon; Cambouropoulos, Emilios; Pease, Alison

COINVENT: Towards a Computational Concept Invention Theory Inproceedings

In: Proceedings of the Fifth International Conference on Computational Creativity, 2014.

Abstract | Links | BibTeX

Colton, Simon; Charnley, John; Pease, Alison

Automated Theory Formation: The Next Generation Journal Article

In: IFCOLOG Journal Proceedings in Computational Logic, 2013.

Abstract | Links | BibTeX

Cavallo, Flaminia; Colton, Simon; Pease, Alison

Uncertainty Modelling in Automated Concept Formation Inproceedings

In: Proceedings of the Automated Reasoning Workshop, pp. 53, Citeseer, 2012.

Abstract | Links | BibTeX

Pease, Alison; Smaill, Alan; Colton, Simon; Ireland, Andrew; Llano, Maria Teresa; Ramezani, Ramin; Grov, Gudmund; Guhe, Markus

Applying Lakatos-style reasoning to AI problems Book Chapter

In: Thinking Machines and the philosophy of computer science: Concepts and principles., Chapter 10, pp. 149–174, Information Science Reference, 2010, ISBN: 9781616920142.

Abstract | Links | BibTeX

Pease, Alison; Colton, Simon; Ramezani, Ramin; Smaill, Alan; Guhe, Markus

Using Analogical Representations for Mathematical Concept Formation Incollection

In: Model-Based Reasoning in Science and Technology, 314 , pp. 301–314, Springer Berlin Heidelberg, 2010, ISBN: 978-3-642-15222-1.

Abstract | Links | BibTeX

Colton, Simon

Three Next Generation Approaches to Automated Mathematical Theory Formation Inproceedings

In: Proceedings of the Model Based Reasoning Conference, 2009.

Abstract | Links | BibTeX

Torres, Pedro; Colton, Simon

First-Order Logic Concept Symmetry for Theory Formation Inproceedings

In: Automated Reasoning Workshop 2009 Bridging the Gap between Theory and Practice, pp. 41, 2009.

Abstract | Links | BibTeX

Pease, Alison; Crook, Paul; Smaill, Alan; Colton, Simon; Guhe, Markus

Towards a Computational Model of Embodied Mathematical Language Book Chapter

In: Proceedings of the Second Symposium on Computing and Philosophy, pp. 35–37, Society for the Study of Artificial Intelligence and Simulation of Behaviour, 2009, ISBN: 1902956826.

Abstract | Links | BibTeX

Torres, Pedro; Colton, Simon

Automated Meta-Theory Induction in Pure Mathematics Incollection

In: Proceedings of the 2008 Automated Reasoning Workshop, 8 , Citeseer, 2008.

Abstract | Links | BibTeX

Colton, Simon; Wagner, Daniel

Using Formal Concept Analysis in Mathematical Discovery Incollection

In: Towards Mechanized Mathematical Assistants, pp. 205–220, Springer, 2007.

Abstract | Links | BibTeX

Torres, Pedro; Colton, Simon

Proving Producibility of Concepts Journal Article

In: 2007.

Abstract | Links | BibTeX

Torres, Pedro; Colton, Simon

Towards Meta-Level Descriptive ILP Inproceedings

In: Proceedings of the 16th International Conference on Inductive Logic Programming, 2006.

Abstract | Links | BibTeX

Colton, Simon; Torres, Pedro; Cairns, Paul; Sorge, Volker

Managing Automatically Formed Mathematical Theories Inproceedings

In: International Conference on Mathematical Knowledge Management, pp. 237–250, Springer 2006.

Abstract | Links | BibTeX

Torres, Pedro; Colton, Simon

Using Model Generation in Automated Concept Formation Inproceedings

In: Proceedings of the Automated Reasoning Workshop, pp. 41, Citeseer, 2006.

Abstract | Links | BibTeX

Pease, Alison; Colton, Simon; Smaill, Alan; Lee, John

A Model of Lakatos’s Philosophy of Mathematics Book

College Publications, 2004.

Abstract | Links | BibTeX

Colton, Simon; Pease, Alison

Lakatos-style Methods in Automated Reasoning Inproceedings

In: In Proceedings of the IJCAI’03 workshop on Agents and Reasoning, Citeseer 2003.

Abstract | Links | BibTeX

Bundy, Alan; Colton, Simon; Huczynska, Sophie; McCasland, Roy

New Directions in Automated Conjecture Making Inproceedings

In: Proceedings of the Automated Reasoning Workshop, 2003.

Abstract | Links | BibTeX

Pease, Alison; Colton, Simon; Smaill, Alan; Lee, John

Semantic Negotiation: Modelling Ambiguity in Dialogue Inproceedings

In: Proceedings of Edilog 2002, the 6th Workshop on the semantics and pragmatics of dialogue, 2002.

Abstract | Links | BibTeX

Pease, Alison; Colton, Simon; Smaill, Alan; Lee, John

Lakatos-style Reasoning Book Chapter

In: Proceedings of the Automated Reasoning Workshop, Imperial College, London, Society for the Study of Artificial Intelligence and Simulation of Behaviour, 2002, ISBN: 1902956265.

Abstract | Links | BibTeX

Pease, Alison; Colton, Simon; Smaill, Alan; Lee, John

A Multi-agent Approach to Modelling Interaction in Human Mathematical Reasoning Inproceedings

In: Proceedings of Intelligent Agent Technology, 2001.

Abstract | Links | BibTeX

Colton, Simon

Experiments in Meta-theory Formation Inproceedings

In: Proceedings of the AISB’01 Symposium on Artificial Intelligence and Creativity in Arts and Science, pp. 100–109, 2001.

Abstract | Links | BibTeX

Colton, Simon

Automated "Plugging and Chugging" Inproceedings

In: Symbolic computation and automated reasoning, pp. 247–248, AK Peters, Ltd. 2001.

Abstract | Links | BibTeX

Colton, Simon

Assessing Exploratory Theory Formation Programs Inproceedings

In: Proceedings of the AAAI-2000 workshop on new research directions in machine learning, 2000.

Abstract | Links | BibTeX

Colton, Simon; Bundy, Alan; Walsh, Toby

Agent Based Cooperative Theory Formation in Pure Mathematics Inproceedings

In: Proceedings of AISB 2000 symposium on creative and cultural aspects and applications of AI and cognitive science, pp. 11–18, 2000.

Abstract | Links | BibTeX

Steel, Graham; Colton, Simon; Bundy, Alan; Walsh, Toby

Cross Domain Mathematical Concept Formation Technical Report

The University of Edinburgh 2000.

Abstract | Links | BibTeX

The Combination of Reasoning Systems

As described above, the HR system for theory formation routinely appeals to third party software as part of its core routine. This led us to address the more general question of when it is possible to combine AI techniques so that the whole is more than a sum of the parts. In total, we have experimented with various combinations of around 20 different AI systems, including descriptive and predictive machine learning systems, model generators, constraint solvers, satisfiability solvers, theorem provers and computer algebra systems. Many of the applications described below make use of a combination of reasoning systems. We have also looked at some more generic ways to combine AI systems. The following papers describe some of our projects in this area:

Colton, Simon

Joined-Up Reasoning for Automated Scientific Discovery: A Position Statement and Research Agenda Inproceedings

In: AAAI Fall Symposium: Automated Scientific Discovery, pp. 18–19, 2008.

Abstract | Links | BibTeX

Charnley, John; Colton, Simon

A Global Workspace Framework for Combining Reasoning Systems Inproceedings

In: International Conference on Intelligent Computer Mathematics, pp. 261–265, Springer Springer Berlin Heidelberg, Berlin, Heidelberg, 2008, ISBN: 978-3-540-85110-3.

Abstract | Links | BibTeX

Charnley, John; Colton, Simon

Applications of a Global Workspace Framework to Mathematical Discovery Inproceedings

In: Proceedings of the Conferences on Intelligent Computer Mathematics workshop on Empirically Successful Automated Reasoning for Mathematics, 2008.

Abstract | Links | BibTeX

Sorge, Volker; Meier, Andreas; McCasland, Roy; Colton, Simon

Integrating AI Systems for Classification in Non-Associative Algebra Inproceedings

In: Proceedings of the 13th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning , Elsevier, 2006.

Abstract | Links | BibTeX

Sorge, Volker; Colton, Simon; Meier, Andreas

A Grid-based Application of Machine Learning to Model Generation Inproceedings

In: Poster Proceedings of KI'04, pp. 204, 2004.

Abstract | Links | BibTeX

Meier, Andreas; Sorge, Volker; Colton, Simon

Employing Theory Formation to Guide Proof Planning Incollection

In: Artificial Intelligence, Automated Reasoning, and Symbolic Computation, pp. 275–289, Springer, 2002.

Abstract | Links | BibTeX

Applications to Discovery Tasks in Pure Mathematics

Pure mathematics is a unique domain for AI research, as mathematical enquiry involves many diverse forms of reasoning, hence we can look at the question of theory formation in pure mathematics and study computational systems which combine different AI techniques. In addition, the data in pure mathematics is usually error free, hence we can concentrate on pure forms of reasoning without (usually) requiring statistical interpretations. On numerous occasions, we have shown that HR and other systems can make mathematical discoveries of genuine value in graph theory, number theory and various algebraic domains of pure mathematics. In addition, by combining HR with multiple other AI systems, we have achieved new partial classifications of algebraic domains, which were previously beyond any computer (or human). The following papers describe some of our projects in this area:

Sorge, Volker; Meier, Andreas; McCasland, Roy; Colton, Simon

Automatic Construction and Verification of Isotopy Invariants Journal Article

In: Journal of Automated Reasoning, 40 (2-3), pp. 221–243, 2008.

Abstract | Links | BibTeX

Sorge, Volker; Colton, Simon; McCasland, Roy; Meier, Andreas

Classification Results in Quasigroup and Loop Theory via a Combination of Automated Reasoning Tools Journal Article

In: Commentationes Mathematicae Universitatis Carolinae, 49 (2), pp. 319–340, 2008.

Abstract | Links | BibTeX

Colton, Simon; Sorge, Volker

Automated Parameterisation of Finite Algebras Inproceedings

In: Workshop on Empirical Successful Automated Reasoning in Mathematics, 2008.

Abstract | Links | BibTeX

Colton, Simon

Computational Discovery in Pure Mathematics Book Chapter

In: Dzeroski, Saso; Todorowski, Ljupco (Ed.): Computational Discovery of Scientific Knowledge, 4660 , pp. 175–201, Springer, 2007.

Abstract | Links | BibTeX

Colton, Simon

Automated Conjecture Making In Number Theory Using HR, Otter and Maple Journal Article

In: Journal of Symbolic Computation, 39 (5), pp. 593–615, 2005.

Abstract | Links | BibTeX

Colton, Simon; Meier, Andreas; Sorge, Volker; McCasland, Roy

Automatic Generation of Classification Theorems for Finite Algebras Inproceedings

In: International Joint Conference on Automated Reasoning, pp. 400–414, Springer 2004.

Abstract | Links | BibTeX

Colton, Simon; Muggleton, Stephen

ILP for Mathematical Discovery Inproceedings

In: International Conference on Inductive Logic Programming, pp. 93–111, Springer 2003.

Abstract | Links | BibTeX

Colton, Simon; Huczynska, Sophie

The HOMER System Inproceedings

In: International Conference on Automated Deduction, pp. 289–294, Springer 2003.

Abstract | Links | BibTeX

Colton, Simon

Making Conjectures About Maple Functions Incollection

In: Artificial Intelligence, Automated Reasoning, and Symbolic Computation, pp. 259–274, Springer, 2002.

Abstract | Links | BibTeX

Colton, Simon; Dennis, Louise Abigail

The NumbersWithNames Program Inproceedings

In: Proceedings of the Seventh AI and Maths Symposium, 2002.

Abstract | Links | BibTeX

Colton, Simon; McCasland, Roy; Bundy, Alan; Walsh, Toby

Automated Theory Formation for Tutoring Tasks in Pure Mathematics Inproceedings

In: In CADE-18, Workshop on the Role of Automated Deduction in Mathematics, Citeseer 2002.

Abstract | Links | BibTeX

Bundy, Alan; Colton, Simon; McCasland, Roy; Walsh, Toby

Semi-Automated Discovery in Zariski Spaces (A Proposal) Inproceedings

In: Proceedings of the Automated Reasoning Workshop, 2002.

Abstract | Links | BibTeX

Colton, Simon

Mathematics - a new Domain for Datamining? Inproceedings

In: Proceedings of the IJCAI-01 Workshop on Knowledge Discovery from Distributed, Dynamic, Heterogenous, Autonomous Sources, 2001.

Abstract | Links | BibTeX

Colton, Simon; Bundy, Alan; Walsh, Toby

Automatic Invention of Integer Sequences Inproceedings

In: AAAI/IAAI, pp. 558–563, 2000.

Abstract | Links | BibTeX

Colton, Simon; Bundy, Alan; Walsh, Toby

On the Notion of Interestingness in Automated Mathematical Discovery Journal Article

In: International Journal of Human-Computer Studies, 53 (3), pp. 351–375, 2000.

Abstract | Links | BibTeX

Colton, Simon; Bundy, Alan; Walsh, Toby

Automated Discovery in Pure Mathematics Inproceedings

In: Automated Reasoning Workshop: Bridging the Gap between Theory and Practice, 1999.

Abstract | Links | BibTeX

Colton, Simon

Refactorable numbers-a machine invention Journal Article

In: Journal of Integer Sequences, 2 (99.1), pp. 2, 1999.

Links | BibTeX

Applications of ATF and Combined Reasoning to Other Domains

While pure mathematics has many advantages, other application domains also stretch the limits of AI systems and their combinations. In order to address the generic nature of the AI systems we have built, we have looked at various non-mathematical applications of ATF. In addition to the projects below, through the supervision of masters projects, we have looked at the usage of HR for musical anomaly detection, for discovery tasks in the gene ontology, for the analysis of board games and the generation of arithmetic puzzles, and for the discovery of software invariants. The following papers describe some of our projects in this area:

Colton, Simon

Countdown Numbers Game: Solved, Analysed, Extended Inproceedings

In: Proceedings of the AISB symposium on AI and Games, 2014.

Abstract | Links | BibTeX

Grov, Gudmund; Farquhar, Colin; Pease, Alison; Colton, Simon

Tinkering by Theory Formation Inproceedings

In: Proceedings of the AIFM workshop, 2014.

Abstract | Links | BibTeX

Cavallo, Flaminia; Pease, Alison; Gow, Jeremy; Colton, Simon

Using Theory Formation Techniques for the Invention of Fictional Concepts Inproceedings

In: Proceedings of the Fourth International Conference on Computational Creativity, pp. 176, 2013.

Abstract | Links | BibTeX

Llano, Maria Teresa; Ireland, Andrew; Pease, Alison; Colton, Simon; Charnley, John

Using Automated Theory Formation to Discover Invariants of Event-B Models Inproceedings

In: In Proceedings of the Rodin User and Developer Workshop, 2010.

Abstract | Links | BibTeX

Baumgarten, Robin; Nika, Maria; Gow, Jeremy; Colton, Simon

Towards the Automatic Invention of Simple Mixed Reality Games Inproceedings

In: Proc. of the AISB’09 Symp. on AI and Games, 2009.

Abstract | Links | BibTeX

Colton, Simon

Automatic Invention of Fitness Functions, with application to Scene Generation Inproceedings

In: Proceedings of the EvoMusArt Workshop, 2008.

Abstract | Links | BibTeX

Jiang, Ning; Colton, Simon

Boosting Descriptive ILP for Predictive Learning in Bioinformatics Inproceedings

In: International Conference on Inductive Logic Programming, pp. 275–289, Springer 2006.

Abstract | Links | BibTeX

Santos, Paulo; Colton, Simon; Magee, Derek

Predictive and Descriptive Approaches to Learning Game Rules from Vision Data Incollection

In: Advances in Artificial Intelligence-IBERAMIA-SBIA 2006, pp. 349–359, Springer, 2006.

Abstract | Links | BibTeX

Colton, Simon

Automated Puzzle Generation Inproceedings

In: Proceedings of the AISB’02 Symposium on AI and Creativity in the Arts and Science, 2002.

Abstract | Links | BibTeX

Colton, Simon

Automated Theory Formation Applied to Mutagenesis Data Inproceedings

In: Proceedings of the First British-Cuban Workshop on BioInformatics, 2002.

Abstract | Links | BibTeX

Improvement of AI Techniques

Given that our overall research goal is to improve the application of AI systems to intelligent tasks, it was sensible for us to question whether combined reasoning systems can improve upon stand-alone systems at standard tasks. Through our experiments with combined reasoning systems, we have shown in many cases that (a) combined reasoning systems can be more flexible in application than stand alone systems (b) combined reasoning systems can be more effective at solving traditional problems than stand alone systems, and (c) combined reasoning systems can undertake intelligent tasks that no single system can attempt. The following papers describe some of our projects in this area:

Ramezani, Ramin; Colton, Simon

Automatic Generation of Dynamic Investigation Problems Inproceedings

In: Proceedings of the Automated Reasoning Workshop, pp. 34, Citeseer 2010.

Abstract | Links | BibTeX

Pease, Alison; Smaill, Alan; Colton, Simon; Ireland, Andrew; Llano, Maria Teresa; Ramezani, Ramin; Grov, Gudmund; Guhe, Markus

Applying Lakatos-style reasoning to AI problems Book Chapter

In: Thinking Machines and the philosophy of computer science: Concepts and principles., Chapter 10, pp. 149–174, Information Science Reference, 2010, ISBN: 9781616920142.

Abstract | Links | BibTeX

Ramezani, Ramin; Colton, Simon

Solving Mutilated Problems Inproceedings

In: Automated Reasoning Workshop, pp. 27, 2009.

Abstract | Links | BibTeX

Charnley, John; Colton, Simon

Prediction using Machine Learned Constraint Satisfaction Programs Inproceedings

In: Proceedings of the Automated Reasoning Workshop, 2007.

Abstract | Links | BibTeX

Charnley, John; Colton, Simon

Expressing General Problems as CSPs Inproceedings

In: Proceedings of the Workshop on Modelling and Solving Problems with Constraints at ECAI, Citeseer 2006.

Abstract | Links | BibTeX

Charnley, John; Colton, Simon; Miguel, Ian

Automated Reformulation of Constraint Satisfaction Problems Inproceedings

In: Proceedings of the Automated Reasoning Workshop, pp. 8, Citeseer, 2006.

Abstract | Links | BibTeX

Charnley, John; Colton, Simon; Miguel, Ian

Automatic generation of Implied Constraints Inproceedings

In: ECAI, pp. 73–77, 2006.

Abstract | Links | BibTeX

Colton, Simon; Pease, Alison

The TM System for Repairing Non-Theorems Journal Article

In: Electronic Notes in Theoretical Computer Science, 125 (3), pp. 87–101, 2005.

Abstract | Links | BibTeX

Colton, Simon; Hoermann, Ferdinand; Sutcliffe, Geoff; Pease, Alison

Machine Learning Case Splits for Theorem Proving Inproceedings

In: Proceedings of the Automated Reasoning Workshop, Edinburgh, 2005.

Abstract | Links | BibTeX

Pease, Alison; Colton, Simon

Automatic Conjecture Modification Book Chapter

In: Proceedings of the 11th Workshop On Automated Reasoning: Bridging The Gap Between Theory And Practice, 2004.

Abstract | Links | BibTeX

Colton, Simon; Pease, Alison

Lakatos-style automated theorem modification Inproceedings

In: ECAI, pp. 977, 2004.

Abstract | Links | BibTeX

Sutcliffe, Geoff; Gao, Yi; Colton, Simon

A Grand Challenge of Theorem Discovery Inproceedings

In: Proceedings of the Workshop on Challenges and Novel Applications for Automated Reasoning, 19th International Conference on Automated Reasoning, pp. 1–11, 2003.

Abstract | Links | BibTeX

Zimmer, Jürgen; Franke, Andreas; Colton, Simon; Sutcliffe, Geoff

Integrating HR and tptp2x into MathWeb to Compare Automated Theorem Provers Inproceedings

In: In Proceedings of the CADE'02 Workshop on Problems and Problem sets, Citeseer 2002.

Abstract | Links | BibTeX

Colton, Simon; Sutcliffe, Geoff

Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems. Inproceedings

In: AMAI, 2002.

Abstract | Links | BibTeX

Colton, Simon

Automated Theorem Discovery: Future Direction for Theorem Provers Miscellaneous

2001.

Abstract | Links | BibTeX

Colton, Simon; Miguel, Ian

Constraint Generation via Automated Theory Formation Inproceedings

In: International Conference on Principles and Practice of Constraint Programming, pp. 575–579, Springer 2001.

Abstract | Links | BibTeX

Colton, Simon

Theory Formation Applied to Learning, Discovery and Problem Solving Inproceedings

In: Proceedings of Machine Intelligence 17, 2000.

Abstract | Links | BibTeX