# 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:

*“Five Next Gen Approaches to Automated Mathematical Theory Formation”*Summer School, Logrogno, 2011

*“Automated Mathematical Theory Formation in a Computational Creativity Context”*EU BISON meeting, London, 2010

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. @inproceedings{GuckelsbergerCHIPlay2017, title = {Predicting Player Experience Without the Player. An Exploratory Study}, author = {Christian Guckelsberger and Christoph Salge and Jeremy Gow and Paul Cairns}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2017/09/ChiPlay2017_PredictingPXWithoutThePlayer_CameraReady_v2.pdf}, year = {2017}, date = {2017-10-01}, booktitle = {Proc. ACM Symp. on Computer-Human Interaction in Play (CHIPlay’17)}, abstract = {A key challenge of procedural content generation (PCG) is to evoke a certain player experience (PX), when we have no direct control over the content which gives rise to that experience. We argue that neither the rigorous methods to assess PX in HCI, nor specialised methods in PCG are sufficient, because they rely on a human in the loop. We propose to address this shortcoming by means of computational models of intrinsic motivation and AI game-playing agents. We hypothesise that our approach could be used to automatically predict PX across games and content types without relying on a human player or designer. We conduct an exploratory study in level generation based on empowerment, a specific model of intrinsic motivation. Based on a thematic analysis, we find that empowerment can be used to create levels with qualitatively different PX. We relate the identified experiences to established theories of PX in HCI and game design, and discuss next steps.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } A key challenge of procedural content generation (PCG) is to evoke a certain player experience (PX), when we have no direct control over the content which gives rise to that experience. We argue that neither the rigorous methods to assess PX in HCI, nor specialised methods in PCG are sufficient, because they rely on a human in the loop. We propose to address this shortcoming by means of computational models of intrinsic motivation and AI game-playing agents. We hypothesise that our approach could be used to automatically predict PX across games and content types without relying on a human player or designer. We conduct an exploratory study in level generation based on empowerment, a specific model of intrinsic motivation. Based on a thematic analysis, we find that empowerment can be used to create levels with qualitatively different PX. We relate the identified experiences to established theories of PX in HCI and game design, and discuss next steps. |

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. @inproceedings{Guckelsberger2017, title = {Addressing the "Why?" in Computational Creativity: A Non-Anthropocentric, Minimal Model of Intentional Creative Agency}, author = {Christian Guckelsberger and Christoph Salge and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2017/05/iccc2017_guckelsberger.pdf}, year = {2017}, date = {2017-05-09}, booktitle = {Proc. 8th Int. Conf. Computational Creativity, 2017 }, abstract = {Generally, computational creativity (CC) systems cannot explain why they are being creative, without ultimately referring back to the values and goals of their designer. Answering the why? would allow for the attribution of intentional agency, and likely lead to a stronger perception of creativity. Enactive artificial intelligence, a framework inspired by autopoietic enactive cognitive science, equips us with the necessary conditions for a value function to reflect a system's own intrinsic goals. We translate the framework's general claims to CC and ground a system's creative activity intrinsically in the maintenance of its identity. We relate to candidate computational principles to realise enactive artificial agents, thus laying the foundations for a minimal, non-anthropocentric model of intentional creative agency. We discuss first implications for the design and evaluation of CC, and address why human-level intentional creative agency is so hard to achieve. We ultimately propose a new research direction in CC, where intentional creative agency is addressed bottom up.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Generally, computational creativity (CC) systems cannot explain why they are being creative, without ultimately referring back to the values and goals of their designer. Answering the why? would allow for the attribution of intentional agency, and likely lead to a stronger perception of creativity. Enactive artificial intelligence, a framework inspired by autopoietic enactive cognitive science, equips us with the necessary conditions for a value function to reflect a system's own intrinsic goals. We translate the framework's general claims to CC and ground a system's creative activity intrinsically in the maintenance of its identity. We relate to candidate computational principles to realise enactive artificial agents, thus laying the foundations for a minimal, non-anthropocentric model of intentional creative agency. We discuss first implications for the design and evaluation of CC, and address why human-level intentional creative agency is so hard to achieve. We ultimately propose a new research direction in CC, where intentional creative agency is addressed bottom up. |

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. @inproceedings{guckelsberger2016c, title = {Intrinsically Motivated General Companion NPCs via Coupled Empowerment Maximisation}, author = {Christian Guckelsberger and Christoph Salge and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/09/guckelsberger_cig16.pdf}, year = {2016}, date = {2016-09-01}, booktitle = {Proc. IEEE Conf. Computational Intelligence in Games (CIG’16)}, publisher = {IEEE}, abstract = {Non-player characters (NPCs) in games are traditionally hard-coded or dependent on pre-specified goals, and consequently struggle to behave sensibly in ever-changing and possibly unpredictable game worlds. To make them fit for new developments in procedural content generation, we introduce the principle of Coupled Empowerment Maximisation as an intrinsic motivation for game NPCs. We focus on the development of a general game companion, designed to support the player in achieving their goals. We evaluate our approach against three intuitive and abstract companion duties. We develop dedicated scenarios for each duty in a dungeon-crawler game testbed, and provide qualitative evidence that the emergent NPC behaviour fulfils these duties. We argue that this generic approach can speed up NPC AI development, improve automatic game evolution and introduce NPCs to full game-generation systems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Non-player characters (NPCs) in games are traditionally hard-coded or dependent on pre-specified goals, and consequently struggle to behave sensibly in ever-changing and possibly unpredictable game worlds. To make them fit for new developments in procedural content generation, we introduce the principle of Coupled Empowerment Maximisation as an intrinsic motivation for game NPCs. We focus on the development of a general game companion, designed to support the player in achieving their goals. We evaluate our approach against three intuitive and abstract companion duties. We develop dedicated scenarios for each duty in a dungeon-crawler game testbed, and provide qualitative evidence that the emergent NPC behaviour fulfils these duties. We argue that this generic approach can speed up NPC AI development, improve automatic game evolution and introduce NPCs to full game-generation systems. |

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. @inproceedings{Guckelsberger2016a, title = {Supportive and Antagonistic Behaviour in Distributed Computational Creativity via Coupled Empowerment Maximisation}, author = {Christian Guckelsberger and Christoph Salge and Rob Saunders and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/06/iccc_camera_ready.pdf}, year = {2016}, date = {2016-07-01}, booktitle = {Proc. 7th Int. Conf. Computational Creativity}, abstract = {There has been a strong tendency in distributed computational creativity systems to embrace embodied and situated agents for their flexible and adaptive behaviour. Intrinsically motivated agents are particularly successful in this respect, because they do not rely on externally specified goals, and can thus react flexibly to changes in open-ended environments. While supportive and antagonistic behaviour is omnipresent when people interact in creative tasks, existing implementations cannot establish such behaviour without constraining their agents’ flexibility by means of explicitly specified interaction rules. More open approaches in contrast cannot guarantee that support or antagonistic behaviour ever comes about. We define the information-theoretic principle of coupled empowerment maximisation as an intrinsically motivated frame for supportive and antagonistic behaviour within which agents can interact with maximum flexibility. We provide an intuition and a formalisation for an arbitrary number of agents. We then draw on several case-studies of co-creative and social creativity systems to make detailed predictions of the potential effect the underlying empowerment maximisation principle might have on the behaviour of creative agents.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } There has been a strong tendency in distributed computational creativity systems to embrace embodied and situated agents for their flexible and adaptive behaviour. Intrinsically motivated agents are particularly successful in this respect, because they do not rely on externally specified goals, and can thus react flexibly to changes in open-ended environments. While supportive and antagonistic behaviour is omnipresent when people interact in creative tasks, existing implementations cannot establish such behaviour without constraining their agents’ flexibility by means of explicitly specified interaction rules. More open approaches in contrast cannot guarantee that support or antagonistic behaviour ever comes about. We define the information-theoretic principle of coupled empowerment maximisation as an intrinsically motivated frame for supportive and antagonistic behaviour within which agents can interact with maximum flexibility. We provide an intuition and a formalisation for an arbitrary number of agents. We then draw on several case-studies of co-creative and social creativity systems to make detailed predictions of the potential effect the underlying empowerment maximisation principle might have on the behaviour of creative agents. |

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. @inproceedings{Guckelsberger2016, title = {Does Empowerment Maximisation Allow for Enactive Artificial Agents?}, author = {Christian Guckelsberger and Christoph Salge}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/06/EmpowermentEnactiveAI_Submission2.pdf}, year = {2016}, date = {2016-07-01}, booktitle = {Proc. 15th Int. Conf. Synthesis and Simulation of Living Systems (ALIFE)}, abstract = {The enactive AI framework wants to overcome the sense making limitations of embodied AI by drawing on the biosystemic foundations of enactive cognitive science. While embodied AI tries to ground meaning in sensorimotor interaction, enactive AI adds further requirements by grounding sensorimotor interaction in autonomous agency. At the core of this shift is the requirement for a truly intrinsic value function. We suggest that empowerment, an information-theoretic quantity based on an agent’s embodiment, represents such a function. We highlight the role of empowerment maximization in satisfying the requirements of enactive AI, i.e. establishing constitutive autonomy and adaptivity, in detail. We then argue that empowerment, grounded in a precarious existence, allows an agent to enact a world based on the relevance of environmental features in respect to its own identity.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The enactive AI framework wants to overcome the sense making limitations of embodied AI by drawing on the biosystemic foundations of enactive cognitive science. While embodied AI tries to ground meaning in sensorimotor interaction, enactive AI adds further requirements by grounding sensorimotor interaction in autonomous agency. At the core of this shift is the requirement for a truly intrinsic value function. We suggest that empowerment, an information-theoretic quantity based on an agent’s embodiment, represents such a function. We highlight the role of empowerment maximization in satisfying the requirements of enactive AI, i.e. establishing constitutive autonomy and adaptivity, in detail. We then argue that empowerment, grounded in a precarious existence, allows an agent to enact a world based on the relevance of environmental features in respect to its own identity. |

#### 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. @inproceedings{schorlemmer2014coinvent, title = {COINVENT: Towards a Computational Concept Invention Theory}, author = { Marco Schorlemmer and Alan Smaill and Kai-Uwe Kühnberger and Oliver Kutz and Simon Colton and Emilios Cambouropoulos and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/shorlemmer_iccc2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the Fifth International Conference on Computational Creativity}, journal = {ICCC}, abstract = {We aim to develop a computationally feasible, cognitively- inspired, formal model of concept invention, drawing on Fauconnier and Turner’s theory of conceptual blending, and grounding it on a sound mathematical theory of concepts. Conceptual blending, although successfully applied to de- scribing combinational creativity in a varied number of fields, has barely been used at all for implementing creative compu- tational systems, mainly due to the lack of sufficiently precise mathematical characterisations thereof. The model we will define will be based on Goguen’s proposal of a Unified Con- cept Theory, and will draw from interdisciplinary research results from cognitive science, artificial intelligence, formal methods and computational creativity. To validate our model, we will implement a proof of concept of an autonomous computational creative system that will be evaluated in two testbed scenarios: mathematical reasoning and melodic har- monisation. We envisage that the results of this project will be significant for gaining a deeper scientific understanding of creativity, for fostering the synergy between understand- ing and enhancing human creativity, and for developing new technologies for autonomous creative systems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We aim to develop a computationally feasible, cognitively- inspired, formal model of concept invention, drawing on Fauconnier and Turner’s theory of conceptual blending, and grounding it on a sound mathematical theory of concepts. Conceptual blending, although successfully applied to de- scribing combinational creativity in a varied number of fields, has barely been used at all for implementing creative compu- tational systems, mainly due to the lack of sufficiently precise mathematical characterisations thereof. The model we will define will be based on Goguen’s proposal of a Unified Con- cept Theory, and will draw from interdisciplinary research results from cognitive science, artificial intelligence, formal methods and computational creativity. To validate our model, we will implement a proof of concept of an autonomous computational creative system that will be evaluated in two testbed scenarios: mathematical reasoning and melodic har- monisation. We envisage that the results of this project will be significant for gaining a deeper scientific understanding of creativity, for fostering the synergy between understand- ing and enhancing human creativity, and for developing new technologies for autonomous creative systems. |

Colton, Simon; Charnley, John; Pease, Alison Automated Theory Formation: The Next Generation Journal Article In: IFCOLOG Journal Proceedings in Computational Logic, 2013. @article{pease2013automated, title = {Automated Theory Formation: The Next Generation}, author = {Simon Colton and John Charnley and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ifcolog15.pdf}, year = {2013}, date = {2013-01-01}, journal = {IFCOLOG Journal Proceedings in Computational Logic}, abstract = {Automated Theory Formation was introduced as a compu- tational model for how mathematical theories could be formed from the bare minimum such as a set of axioms or some background concepts in a domain of pure mathematics such as group theory, graph theory or num- ber theory. The approach consists of using production rules to form new concepts from old ones, and employing a set of measures of interesting- ness to drive a heuristic search. Empirical pattern-based conjecture mak- ing techniques are used to find relationships between concepts, and third party automated reasoning systems are employed to prove the truth of the conjectures or find counterexamples. Automated Theory Formation has been applied to a number of discovery tasks which have led to the publication of mathematical results in the literature. In recent years, the approach has been extended, improved and generalised. This has been done via appeals to the philosophy of mathematics, namely Lakatos’s suggestions in the book Proofs and Refutations describing ways in which mathematicians find and respond to counterexamples, using them to evolve concepts, conjectures and proofs within a mathematical theory. The resulting computational approach extends Automated Theory For- mation by modelling ways in which mathematicians discuss counterex- amples and their implications for the conjecture at hand. The recent extensions also appeal to cognitive science results, in particular Baar’s suggestions in the Global Workspace Architecture theory of mammalian consciousness. The resulting computational approach involves configur- ing a framework for the combination of reasoning systems leading to more sophisticated and applied theory formation approaches. We sur- vey these extensions here, in addition to other projects that have added to our understanding of Automated Theory Formation. We also frame these approaches within a broader picture, specifically with reference to Mathematical Theory Exploration approaches. We end with a discussion of future applications and extensions of Automated Theory Formation.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Automated Theory Formation was introduced as a compu- tational model for how mathematical theories could be formed from the bare minimum such as a set of axioms or some background concepts in a domain of pure mathematics such as group theory, graph theory or num- ber theory. The approach consists of using production rules to form new concepts from old ones, and employing a set of measures of interesting- ness to drive a heuristic search. Empirical pattern-based conjecture mak- ing techniques are used to find relationships between concepts, and third party automated reasoning systems are employed to prove the truth of the conjectures or find counterexamples. Automated Theory Formation has been applied to a number of discovery tasks which have led to the publication of mathematical results in the literature. In recent years, the approach has been extended, improved and generalised. This has been done via appeals to the philosophy of mathematics, namely Lakatos’s suggestions in the book Proofs and Refutations describing ways in which mathematicians find and respond to counterexamples, using them to evolve concepts, conjectures and proofs within a mathematical theory. The resulting computational approach extends Automated Theory For- mation by modelling ways in which mathematicians discuss counterex- amples and their implications for the conjecture at hand. The recent extensions also appeal to cognitive science results, in particular Baar’s suggestions in the Global Workspace Architecture theory of mammalian consciousness. The resulting computational approach involves configur- ing a framework for the combination of reasoning systems leading to more sophisticated and applied theory formation approaches. We sur- vey these extensions here, in addition to other projects that have added to our understanding of Automated Theory Formation. We also frame these approaches within a broader picture, specifically with reference to Mathematical Theory Exploration approaches. We end with a discussion of future applications and extensions of Automated Theory Formation. |

Cavallo, Flaminia; Colton, Simon; Pease, Alison Uncertainty Modelling in Automated Concept Formation Inproceedings In: Proceedings of the Automated Reasoning Workshop, pp. 53, Citeseer, 2012. @inproceedings{cavallo2012uncertainty, title = {Uncertainty Modelling in Automated Concept Formation}, author = { Flaminia Cavallo and Simon Colton and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/cavallo_arw12.pdf}, year = {2012}, date = {2012-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, journal = {ARW 2012}, pages = {53}, publisher = {Citeseer}, abstract = {Categorisation and classification are areas that have been well studied in machine learning. How- ever, the use of cognitive theories in psychology as a basis to implement a category formation system designed for creative purposes and based on human behaviour is still largely unexplored. Our aim in this project is to verify how some of the ideas on uncertainty and ambiguity in classification could influence concept classifica- tion in an automated theory formation system.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Categorisation and classification are areas that have been well studied in machine learning. How- ever, the use of cognitive theories in psychology as a basis to implement a category formation system designed for creative purposes and based on human behaviour is still largely unexplored. Our aim in this project is to verify how some of the ideas on uncertainty and ambiguity in classification could influence concept classifica- tion in an automated theory formation system. |

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. @inbook{pease2010applying, title = {Applying Lakatos-style reasoning to AI problems}, author = {Alison Pease and Alan Smaill and Simon Colton and Andrew Ireland and Maria Teresa Llano and Ramin Ramezani and Gudmund Grov and Markus Guhe}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_tm10-1.pdf}, doi = {10.4018/978-1-61692-014-2.ch010}, isbn = {9781616920142}, year = {2010}, date = {2010-01-01}, booktitle = {Thinking Machines and the philosophy of computer science: Concepts and principles.}, journal = {Thinking Machines and the philosophy of computer science: Concepts and principles}, pages = {149--174}, publisher = {Information Science Reference}, chapter = {10}, abstract = {One current direction in AI research is to focus on combining different reasoning styles such as deduction, induction, abduction, analogical reasoning, non-monotonic reasoning, vague and uncertain reasoning. The philosopher Imre Lakatos produced one such theory of how people with different reasoning styles collaborate to develop mathematical ideas. Lakatos argued that mathematics is a quasi-empirical, flexible, fallible, human endeavour, involving negotiations, mistakes, vague concept definitions and disagreements, and he outlined a heuristic approach towards the subject. In this chapter we apply these heuristics to the AI domains of evolving requirement specifi- cations, planning and constraint satisfaction problems. In drawing analogies between Lakatos’s theory and these three domains we identify areas of work which correspond to each heuristic, and suggest extensions and further ways in which Lakatos’s philoso- phy can inform AI problem solving. Thus, we show how we might begin to produce a philosophically-inspired AI theory of combined reasoning.}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } One current direction in AI research is to focus on combining different reasoning styles such as deduction, induction, abduction, analogical reasoning, non-monotonic reasoning, vague and uncertain reasoning. The philosopher Imre Lakatos produced one such theory of how people with different reasoning styles collaborate to develop mathematical ideas. Lakatos argued that mathematics is a quasi-empirical, flexible, fallible, human endeavour, involving negotiations, mistakes, vague concept definitions and disagreements, and he outlined a heuristic approach towards the subject. In this chapter we apply these heuristics to the AI domains of evolving requirement specifi- cations, planning and constraint satisfaction problems. In drawing analogies between Lakatos’s theory and these three domains we identify areas of work which correspond to each heuristic, and suggest extensions and further ways in which Lakatos’s philoso- phy can inform AI problem solving. Thus, we show how we might begin to produce a philosophically-inspired AI theory of combined reasoning. |

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. @incollection{pease2010using, title = {Using Analogical Representations for Mathematical Concept Formation}, author = { Alison Pease and Simon Colton and Ramin Ramezani and Alan Smaill and Markus Guhe}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_mbr10.pdf}, doi = {10.1007/978-3-642-15223-8}, isbn = {978-3-642-15222-1}, year = {2010}, date = {2010-01-01}, booktitle = {Model-Based Reasoning in Science and Technology}, volume = {314}, pages = {301--314}, publisher = {Springer Berlin Heidelberg}, abstract = {We argue that visual, analogical representations of mathematical concepts can be used by automated theory formation systems to develop fur- ther concepts and conjectures in mathematics. We consider the role of visual reasoning in human development of mathematics, and consider some aspects of the relationship between mathematics and the visual, including artists us- ing mathematics as inspiration for their art (which may then feed back into mathematical development), the idea of using visual beauty to evaluate math- ematics, mathematics which is visually pleasing, and ways of using the visual to develop mathematical concepts. We motivate an analogical representation of number types with examples of “visual” concepts and conjectures, and present an automated case study in which we enable an automated theory formation program to read this type of visual, analogical representation.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } We argue that visual, analogical representations of mathematical concepts can be used by automated theory formation systems to develop fur- ther concepts and conjectures in mathematics. We consider the role of visual reasoning in human development of mathematics, and consider some aspects of the relationship between mathematics and the visual, including artists us- ing mathematics as inspiration for their art (which may then feed back into mathematical development), the idea of using visual beauty to evaluate math- ematics, mathematics which is visually pleasing, and ways of using the visual to develop mathematical concepts. We motivate an analogical representation of number types with examples of “visual” concepts and conjectures, and present an automated case study in which we enable an automated theory formation program to read this type of visual, analogical representation. |

Colton, Simon Three Next Generation Approaches to Automated Mathematical Theory Formation Inproceedings In: Proceedings of the Model Based Reasoning Conference, 2009. @inproceedings{Colton2009, title = {Three Next Generation Approaches to Automated Mathematical Theory Formation}, author = {Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_mbr09.pdf}, year = {2009}, date = {2009-08-01}, booktitle = {Proceedings of the Model Based Reasoning Conference}, abstract = {Around a decade ago, we introduced Automated Theory Formation as a technique for mathematical discovery, implemented in the HR system. Starting with some basic background information such as a set of axioms for an algebraic domain, or fundamental concepts such as addition and multiplication in number theory, HR forms concepts which categorise the examples; makes conjectures which relate the concepts; and generates proofs which explain the conjectures (or counterexamples which disprove them). In addition to inventing concepts and discovering theorems which have been published in the mathematical literature, HR has been applied successfully to AI tasks including constraint solving and machine learning. In the talk, I will describe three PhD projects which have been influenced by the Automated Theory Formation approach.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Around a decade ago, we introduced Automated Theory Formation as a technique for mathematical discovery, implemented in the HR system. Starting with some basic background information such as a set of axioms for an algebraic domain, or fundamental concepts such as addition and multiplication in number theory, HR forms concepts which categorise the examples; makes conjectures which relate the concepts; and generates proofs which explain the conjectures (or counterexamples which disprove them). In addition to inventing concepts and discovering theorems which have been published in the mathematical literature, HR has been applied successfully to AI tasks including constraint solving and machine learning. In the talk, I will describe three PhD projects which have been influenced by the Automated Theory Formation approach. |

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. @inproceedings{torres2009first, title = {First-Order Logic Concept Symmetry for Theory Formation}, author = { Pedro Torres and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/torres_arw09.pdf}, year = {2009}, date = {2009-01-07}, booktitle = {Automated Reasoning Workshop 2009 Bridging the Gap between Theory and Practice}, pages = {41}, abstract = {SURICATA (Torres and Colton, 2008) is a hybrid automated theory formation system which uses both production rules and structured language biased search to produce new concepts and make conjectures about those concepts. The idea of implementing a highly-configurable theory formation system able to work with arbitrary first-order production rules started from the observation that it was helpful for users of automated theory formation systems to be able to define their own production rules. We implemented a generic first-order production rule (Torres and Colton, 2006) for the HR system (Colton, 2002) and showed how new user-defined production rules led to the discovery of novel conjectures in quasigroup theory.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } SURICATA (Torres and Colton, 2008) is a hybrid automated theory formation system which uses both production rules and structured language biased search to produce new concepts and make conjectures about those concepts. The idea of implementing a highly-configurable theory formation system able to work with arbitrary first-order production rules started from the observation that it was helpful for users of automated theory formation systems to be able to define their own production rules. We implemented a generic first-order production rule (Torres and Colton, 2006) for the HR system (Colton, 2002) and showed how new user-defined production rules led to the discovery of novel conjectures in quasigroup theory. |

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. @inbook{Pease2009, title = {Towards a Computational Model of Embodied Mathematical Language}, author = { Alison Pease and Paul Crook and Alan Smaill and Simon Colton and Markus Guhe}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_aisb09.pdf}, isbn = {1902956826}, year = {2009}, date = {2009-01-01}, booktitle = {Proceedings of the Second Symposium on Computing and Philosophy}, pages = {35--37}, publisher = {Society for the Study of Artificial Intelligence and Simulation of Behaviour}, abstract = {We outline two theories of mathematical language acquisition and development, and discuss how a computational model of these theories may help to bridge the gap between automated theory formation and situated embodied agents. Finally, we briefly describe a simple theoretical case study of how such a model could work in the arithmetic domain.}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } We outline two theories of mathematical language acquisition and development, and discuss how a computational model of these theories may help to bridge the gap between automated theory formation and situated embodied agents. Finally, we briefly describe a simple theoretical case study of how such a model could work in the arithmetic domain. |

Torres, Pedro; Colton, Simon Automated Meta-Theory Induction in Pure Mathematics Incollection In: Proceedings of the 2008 Automated Reasoning Workshop, 8 , Citeseer, 2008. @incollection{torres2008automated, title = {Automated Meta-Theory Induction in Pure Mathematics}, author = { Pedro Torres and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/torres_arw08.pdf}, year = {2008}, date = {2008-01-01}, booktitle = {Proceedings of the 2008 Automated Reasoning Workshop}, journal = {Proceedings of ARW}, volume = {8}, publisher = {Citeseer}, abstract = {HR [1] is an Automated Theory Formation (ATF) system which has been described as a Descriptive Inductive Logic Programming system [4]. Given a set of initial concepts, each provided with a definition and a set of examples, HR forms a theory about them. HR uses a set of production rules to form new concepts and forms conjectures according to the examples it finds for new concepts.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } HR [1] is an Automated Theory Formation (ATF) system which has been described as a Descriptive Inductive Logic Programming system [4]. Given a set of initial concepts, each provided with a definition and a set of examples, HR forms a theory about them. HR uses a set of production rules to form new concepts and forms conjectures according to the examples it finds for new concepts. |

Colton, Simon; Wagner, Daniel Using Formal Concept Analysis in Mathematical Discovery Incollection In: Towards Mechanized Mathematical Assistants, pp. 205–220, Springer, 2007. @incollection{colton2007using, title = {Using Formal Concept Analysis in Mathematical Discovery}, author = { Simon Colton and Daniel Wagner}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_mkm07.pdf}, year = {2007}, date = {2007-01-01}, booktitle = {Towards Mechanized Mathematical Assistants}, pages = {205--220}, publisher = {Springer}, abstract = {Formal concept analysis (FCA) comprises a set of powerful algorithms which can be used for data analysis and manipulation, and a set of visualisation tools which enable the discovery of meaningful re- lationships between attributes of the data. We explore the potential of combining FCA and mathematical discovery tools in order to better fa- cilitate discovery tasks. In particular, we propose a novel lookup method for the Encyclopedia of Integer Sequences, and we show how conjectures from the Graffiti discovery program can be better understood using FCA visualisation tools. We argue that, not only can FCA tools greatly en- hance the management and visualisation of mathematical knowledge, but they can also be used to drive exploratory processes.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } Formal concept analysis (FCA) comprises a set of powerful algorithms which can be used for data analysis and manipulation, and a set of visualisation tools which enable the discovery of meaningful re- lationships between attributes of the data. We explore the potential of combining FCA and mathematical discovery tools in order to better fa- cilitate discovery tasks. In particular, we propose a novel lookup method for the Encyclopedia of Integer Sequences, and we show how conjectures from the Graffiti discovery program can be better understood using FCA visualisation tools. We argue that, not only can FCA tools greatly en- hance the management and visualisation of mathematical knowledge, but they can also be used to drive exploratory processes. |

Torres, Pedro; Colton, Simon Proving Producibility of Concepts Journal Article In: 2007. @article{producibilityproving, title = {Proving Producibility of Concepts}, author = {Pedro Torres and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/torres_arw07.pdf}, year = {2007}, date = {2007-01-01}, publisher = {Citeseer}, abstract = {In a previous study (Torres and Colton, 2006a), we presented a general framework for using model generation to implement generic first-order production rules. We have taken this idea one step further by designing a general automated theory formation system which is able to deal with arbitrary sets of first-order production rules. In the same study, we also sketched a method of backwards proof to prove concept producibility which we will here put to practice. In this workshop we will address both unsolved problems mentioned above by (i) presenting an algorithm for proving producibility of concepts by our theory formation system and (ii) putting forward ideas on how this algorithm may be useful to induce production rules from examples of produced concepts.}, keywords = {}, pubstate = {published}, tppubtype = {article} } In a previous study (Torres and Colton, 2006a), we presented a general framework for using model generation to implement generic first-order production rules. We have taken this idea one step further by designing a general automated theory formation system which is able to deal with arbitrary sets of first-order production rules. In the same study, we also sketched a method of backwards proof to prove concept producibility which we will here put to practice. In this workshop we will address both unsolved problems mentioned above by (i) presenting an algorithm for proving producibility of concepts by our theory formation system and (ii) putting forward ideas on how this algorithm may be useful to induce production rules from examples of produced concepts. |

Torres, Pedro; Colton, Simon Towards Meta-Level Descriptive ILP Inproceedings In: Proceedings of the 16th International Conference on Inductive Logic Programming, 2006. @inproceedings{torres2006towards, title = {Towards Meta-Level Descriptive ILP}, author = { Pedro Torres and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/torres_ilp06poster.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of the 16th International Conference on Inductive Logic Programming}, abstract = {We introduce a formal setting for a first-order production rule approach to descriptive learning and we consider searching for sets of production rules as opposed to a direct search for concepts. We sketch the Parrot algorithm which generates a basic set of production rules capable of producing a set of user-given concepts and present some pre- liminary ideas on how to enrich this set.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We introduce a formal setting for a first-order production rule approach to descriptive learning and we consider searching for sets of production rules as opposed to a direct search for concepts. We sketch the Parrot algorithm which generates a basic set of production rules capable of producing a set of user-given concepts and present some pre- liminary ideas on how to enrich this set. |

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. @inproceedings{colton2006managing, title = {Managing Automatically Formed Mathematical Theories}, author = { Simon Colton and Pedro Torres and Paul Cairns and Volker Sorge}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_mkm06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {International Conference on Mathematical Knowledge Management}, pages = {237--250}, organization = {Springer}, abstract = {The HR system forms scientific theories, and has found par- ticularly successful application in domains of pure mathematics. Starting with only the axioms of an algebraic system, HR can generate dozens of example algebras, hundreds of concepts and thousands of conjectures, many of which have first order proofs. Given the overwhelming amount of knowledge produced, we have provided HR with sophisticated tools for handling this data. We present here the first full description of these management tools. Moreover, we describe how careful analysis of the theories produced by HR – which is enabled by the management tools – has led us to make interesting discoveries in algebraic domains. We demonstrate this with some illustrative results from HR’s theories about an algebra of one axiom. The results fueled further developments, and led us to discover and prove a fundamental theorem about this domain.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The HR system forms scientific theories, and has found par- ticularly successful application in domains of pure mathematics. Starting with only the axioms of an algebraic system, HR can generate dozens of example algebras, hundreds of concepts and thousands of conjectures, many of which have first order proofs. Given the overwhelming amount of knowledge produced, we have provided HR with sophisticated tools for handling this data. We present here the first full description of these management tools. Moreover, we describe how careful analysis of the theories produced by HR – which is enabled by the management tools – has led us to make interesting discoveries in algebraic domains. We demonstrate this with some illustrative results from HR’s theories about an algebra of one axiom. The results fueled further developments, and led us to discover and prove a fundamental theorem about this domain. |

Torres, Pedro; Colton, Simon Using Model Generation in Automated Concept Formation Inproceedings In: Proceedings of the Automated Reasoning Workshop, pp. 41, Citeseer, 2006. @inproceedings{torres2006using, title = {Using Model Generation in Automated Concept Formation}, author = { Pedro Torres and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/torres_arw06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, journal = {Specification and Verification of Reconfiguration Protocols in Grid Component Systems}, pages = {41}, publisher = {Citeseer}, abstract = {HR (Colton, 2002) is an Automated Theory Formation (ATF) system which makes extensive use of automated reasoning tools, in particular, the Otter theorem prover (McCune, 1990) and MACE model generator (McCune, 1994). Given a set of initial concepts, each provided with a definition and a set of examples, HR forms a theory about them. HR uses a set of production rules to form new concepts and forms conjectures according to the examples it finds for new concepts. For instance, if the set of examples for the new concept is contained in the set of examples of some old concept, an implication conjecture is generated. Similarly, equivalence and non-existence conjectures can be made. We present here a general first order setting for concept production in ATF, explain a recently implemented user-customisable generic production rule, and report on results in pure mathematics obtained using the new rule. The new concept production method make novel use of MACE, thus extending the combination of reasoning techniques employed in theory formation.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } HR (Colton, 2002) is an Automated Theory Formation (ATF) system which makes extensive use of automated reasoning tools, in particular, the Otter theorem prover (McCune, 1990) and MACE model generator (McCune, 1994). Given a set of initial concepts, each provided with a definition and a set of examples, HR forms a theory about them. HR uses a set of production rules to form new concepts and forms conjectures according to the examples it finds for new concepts. For instance, if the set of examples for the new concept is contained in the set of examples of some old concept, an implication conjecture is generated. Similarly, equivalence and non-existence conjectures can be made. We present here a general first order setting for concept production in ATF, explain a recently implemented user-customisable generic production rule, and report on results in pure mathematics obtained using the new rule. The new concept production method make novel use of MACE, thus extending the combination of reasoning techniques employed in theory formation. |

Pease, Alison; Colton, Simon; Smaill, Alan; Lee, John A Model of Lakatos’s Philosophy of Mathematics Book College Publications, 2004. @book{pease2004model, title = {A Model of Lakatos’s Philosophy of Mathematics}, author = { Alison Pease and Simon Colton and Alan Smaill and John Lee}, editor = {Lorenzo Magnani and Riccardo Dossena}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_ecap04.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {Computing, Philosophy and Cognition}, publisher = {College Publications}, series = {Texts in philosophy}, abstract = {Lakatos attacked the view that mathematical knowledge is timeless, certain and a priori (Lakatos, 1976). Lakatos's work in the philosophy of mathematics is a controversial mathematical analogy of Hume's problem of induction combined with Popper's theory of falsification. That is, Lakatos both identified the problem of the impossibility of mathematical knowledge, and suggested a solution. His solution consisted of heuristic methods which guide the development of mathematical conjectures, concepts and proofs. These evolve through dialectic and analysis sparked by counterexamples. Counterexamples therefore, play a vital role in (Lakatos, 1976), though they are a starting, rather than finishing point: criticism has to be constructive if it is to be valuable. }, keywords = {}, pubstate = {published}, tppubtype = {book} } Lakatos attacked the view that mathematical knowledge is timeless, certain and a priori (Lakatos, 1976). Lakatos's work in the philosophy of mathematics is a controversial mathematical analogy of Hume's problem of induction combined with Popper's theory of falsification. That is, Lakatos both identified the problem of the impossibility of mathematical knowledge, and suggested a solution. His solution consisted of heuristic methods which guide the development of mathematical conjectures, concepts and proofs. These evolve through dialectic and analysis sparked by counterexamples. Counterexamples therefore, play a vital role in (Lakatos, 1976), though they are a starting, rather than finishing point: criticism has to be constructive if it is to be valuable. |

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. @inproceedings{colton2003lakatos, title = {Lakatos-style Methods in Automated Reasoning}, author = { Simon Colton and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ijcai03_agents.pdf}, year = {2003}, date = {2003-01-01}, booktitle = {In Proceedings of the IJCAI’03 workshop on Agents and Reasoning}, organization = {Citeseer}, abstract = {We advocate increased flexibility in automated reasoning, whereby a reasoning agent is able to correct the statement of a given faulty conjec-ture in order to prove that the modified the-orem is true. Such alterations are common in mathematics. In particular, in his book 'Proofs and Refutations', Imre Lakatos prescribes var-ious techniques for the modification of a faulty conjecture within a social setting (a hypothe-sised mathematics class). This has inspired a multi-agent approach to automating Lakatos-style techniques, and we give details of the implementation of these methods within (and on top of) the HR automated theory forma-tion system. We report on the progress of this project and supply illustrative results from ses-sions using the enhanced system. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We advocate increased flexibility in automated reasoning, whereby a reasoning agent is able to correct the statement of a given faulty conjec-ture in order to prove that the modified the-orem is true. Such alterations are common in mathematics. In particular, in his book 'Proofs and Refutations', Imre Lakatos prescribes var-ious techniques for the modification of a faulty conjecture within a social setting (a hypothe-sised mathematics class). This has inspired a multi-agent approach to automating Lakatos-style techniques, and we give details of the implementation of these methods within (and on top of) the HR automated theory forma-tion system. We report on the progress of this project and supply illustrative results from ses-sions using the enhanced system. |

Bundy, Alan; Colton, Simon; Huczynska, Sophie; McCasland, Roy New Directions in Automated Conjecture Making Inproceedings In: Proceedings of the Automated Reasoning Workshop, 2003. @inproceedings{Bundy2003, title = {New Directions in Automated Conjecture Making}, author = {Alan Bundy and Simon Colton and Sophie Huczynska and Roy McCasland}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/bundy_arw03.pdf}, year = {2003}, date = {2003-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, abstract = {The HR system has been developed to form scientific theories automatically, with special application to mathematical conjecture making [1]. Two projects with HR are currently coming to an end and within both, there have been recent studies of the potential application of HR to research mathematics. These studies have led to some criticisms about the current limitations of HR and suggestions for improvements. Furthermore, a new project with a goal of extending HR in order to test its application to an area of research mathematics is about to start. Hence, now is a ideal time to look at these criticisms and recommendations and suggest directions for the future development of the system, which we do here. To appreciate the recommendations, we first give a brief overview of the theory formation HR undertakes. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The HR system has been developed to form scientific theories automatically, with special application to mathematical conjecture making [1]. Two projects with HR are currently coming to an end and within both, there have been recent studies of the potential application of HR to research mathematics. These studies have led to some criticisms about the current limitations of HR and suggestions for improvements. Furthermore, a new project with a goal of extending HR in order to test its application to an area of research mathematics is about to start. Hence, now is a ideal time to look at these criticisms and recommendations and suggest directions for the future development of the system, which we do here. To appreciate the recommendations, we first give a brief overview of the theory formation HR undertakes. |

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. @inproceedings{pease2002semantic, title = {Semantic Negotiation: Modelling Ambiguity in Dialogue}, author = { Alison Pease and Simon Colton and Alan Smaill and John Lee}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_edilog02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Proceedings of Edilog 2002, the 6th Workshop on the semantics and pragmatics of dialogue}, abstract = {We argue that negotiation over the meaning of terms in a statement is part of human discussion and that it can lead to richer theories. We describe our pre-liminary model of semantic negotiation and discuss theoretical examples which we hope to implement. Finally we consider how semantic negotiation fits into existing work on argumentation. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We argue that negotiation over the meaning of terms in a statement is part of human discussion and that it can lead to richer theories. We describe our pre-liminary model of semantic negotiation and discuss theoretical examples which we hope to implement. Finally we consider how semantic negotiation fits into existing work on argumentation. |

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. @inbook{Pease2002, title = {Lakatos-style Reasoning}, author = {Alison Pease and Simon Colton and Alan Smaill and John Lee}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_arw02.pdf}, isbn = {1902956265}, year = {2002}, date = {2002-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop, Imperial College, London}, publisher = {Society for the Study of Artificial Intelligence and Simulation of Behaviour}, abstract = {A problem in modelling mathematics is that few people have analysed and reported the way in which mathematicians work. Lakatos(4) is a welcome exception. He presents a rational recon-struction of the evolution of Euler's conjecture that for all polyhedra, the number of vertices (V) minus the number of edges (E) plus the number of faces (F) is two, and its proof. This work spans 200 years of concepts, conjectures, counter-examples and 'proofs' and is invaluable to AI researchers trying to model mathematical reasoning. Such models might serve to (a) illuminate aspects of human mathematics, and (b) improve existing automated reasoning programs.}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } A problem in modelling mathematics is that few people have analysed and reported the way in which mathematicians work. Lakatos(4) is a welcome exception. He presents a rational recon-struction of the evolution of Euler's conjecture that for all polyhedra, the number of vertices (V) minus the number of edges (E) plus the number of faces (F) is two, and its proof. This work spans 200 years of concepts, conjectures, counter-examples and 'proofs' and is invaluable to AI researchers trying to model mathematical reasoning. Such models might serve to (a) illuminate aspects of human mathematics, and (b) improve existing automated reasoning programs. |

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. @inproceedings{pease2001multi, title = {A Multi-agent Approach to Modelling Interaction in Human Mathematical Reasoning}, author = { Alison Pease and Simon Colton and Alan Smaill and John Lee}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_iat01.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {Proceedings of Intelligent Agent Technology}, journal = {Intelligent Agent Technology Research and Development}, abstract = {Current work in automated reasoning does not in general model social aspects of human mathematics, with a few exceptions, for example [1]. We are inter-ested in modelling concept and conjecture refinement, i.e. the way in which the definition of a concept evolves as a conjecture develops. Modelling this process is important because (a) it will illuminate aspects of the social nature of mathematics and (b) it may be useful for improving existing automated reasoning programs. In V we outline descriptions by Devlin and Lakatos of the human process. In 9 we describe an agent architecture for this task and how it could be implemented using the HR theory formation system[2]. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Current work in automated reasoning does not in general model social aspects of human mathematics, with a few exceptions, for example [1]. We are inter-ested in modelling concept and conjecture refinement, i.e. the way in which the definition of a concept evolves as a conjecture develops. Modelling this process is important because (a) it will illuminate aspects of the social nature of mathematics and (b) it may be useful for improving existing automated reasoning programs. In V we outline descriptions by Devlin and Lakatos of the human process. In 9 we describe an agent architecture for this task and how it could be implemented using the HR theory formation system[2]. |

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. @inproceedings{colton2001experiments, title = {Experiments in Meta-theory Formation}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aisb01.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {Proceedings of the AISB’01 Symposium on Artificial Intelligence and Creativity in Arts and Science}, pages = {100--109}, abstract = {An ability to reason at a meta-level is widely regarded as an important aspect of human creativity which is often missing from creative computer programs. We discuss recent experiments with the HR theory formation program where it formed meta-theories about previously formed theories. We report how HR re-invented aspects of how it forms theories and reflected on the nature of the theories it produces. Additionally, the meta-theories contains higher level concepts than those produced using HR normally. We discuss how HR’s meta-level abilities were enabled by changing domains, rather than writing new programs, which was the model previously employed in the Meta-DENDRAL and Eurisko programs. These experiments suggest an improved model of theory formation where meta-theories are produced alongside theories, with information from the meta-theory being used to improve the search in the original theory.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } An ability to reason at a meta-level is widely regarded as an important aspect of human creativity which is often missing from creative computer programs. We discuss recent experiments with the HR theory formation program where it formed meta-theories about previously formed theories. We report how HR re-invented aspects of how it forms theories and reflected on the nature of the theories it produces. Additionally, the meta-theories contains higher level concepts than those produced using HR normally. We discuss how HR’s meta-level abilities were enabled by changing domains, rather than writing new programs, which was the model previously employed in the Meta-DENDRAL and Eurisko programs. These experiments suggest an improved model of theory formation where meta-theories are produced alongside theories, with information from the meta-theory being used to improve the search in the original theory. |

Colton, Simon Automated "Plugging and Chugging" Inproceedings In: Symbolic computation and automated reasoning, pp. 247–248, AK Peters, Ltd. 2001. @inproceedings{colton2001automated, title = {Automated "Plugging and Chugging"}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_calculemus00.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {Symbolic computation and automated reasoning}, pages = {247--248}, organization = {AK Peters, Ltd.}, abstract = {In [1], Paul Zeitz discusses how to solve mathematical problems. One tech-nique he proposes is to calculate some examples of objects in the problem statement and try to spot a pattern or property which provides insight into the nature of the problem.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In [1], Paul Zeitz discusses how to solve mathematical problems. One tech-nique he proposes is to calculate some examples of objects in the problem statement and try to spot a pattern or property which provides insight into the nature of the problem. |

Colton, Simon Assessing Exploratory Theory Formation Programs Inproceedings In: Proceedings of the AAAI-2000 workshop on new research directions in machine learning, 2000. @inproceedings{colton2000assessing, title = {Assessing Exploratory Theory Formation Programs}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aaai00w.pdf}, year = {2000}, date = {2000-01-01}, booktitle = {Proceedings of the AAAI-2000 workshop on new research directions in machine learning}, abstract = {Broadly speaking, machine learning programs are asked to identify a single concept given a set of examples and some background knowledge. Mathematical theory form- ation programs, such as the AM program, (Davis & Lenat 1982) and the HR program, (Colton, Bundy, & Walsh 1999), are also given a set of examples and some background know- ledge. However, they are not asked to find a single concept, but rather to explore the domain and attempt to gain some understanding of it. Because the domain is mathematics, there are a range of ways by which the program can gain an understanding of the domain, including inventing concepts, performing calculations, making conjectures, proving theor- ems and finding counterexamples. The HR system is able to perform all of these activities in domains such as group the- ory, where it employs the Otter theorem prover, (McCune 1990), and MACE counterexample finder, (McCune 1994), to prove and disprove theorems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Broadly speaking, machine learning programs are asked to identify a single concept given a set of examples and some background knowledge. Mathematical theory form- ation programs, such as the AM program, (Davis & Lenat 1982) and the HR program, (Colton, Bundy, & Walsh 1999), are also given a set of examples and some background know- ledge. However, they are not asked to find a single concept, but rather to explore the domain and attempt to gain some understanding of it. Because the domain is mathematics, there are a range of ways by which the program can gain an understanding of the domain, including inventing concepts, performing calculations, making conjectures, proving theor- ems and finding counterexamples. The HR system is able to perform all of these activities in domains such as group the- ory, where it employs the Otter theorem prover, (McCune 1990), and MACE counterexample finder, (McCune 1994), to prove and disprove theorems. |

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. @inproceedings{colton2000agent, title = {Agent Based Cooperative Theory Formation in Pure Mathematics}, author = { Simon Colton and Alan Bundy and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aisb00.pdf}, year = {2000}, date = {2000-01-01}, booktitle = {Proceedings of AISB 2000 symposium on creative and cultural aspects and applications of AI and cognitive science}, pages = {11--18}, abstract = {The HR program, Colton et al. (1999), performs theory formation in domains of pure mathematics. Given only minimal information about a domain, it invents concepts, make conjectures, proves theorems and finds counterexamples to false conjectures. We present here a multi-agent version of HR which may provide a model for how individual mathematicians perform separate investigations but communicate their results to the mathematical community, learning from others as they do. We detail the exhaustive categorisation problem to which we have applied a multi-agent approach.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The HR program, Colton et al. (1999), performs theory formation in domains of pure mathematics. Given only minimal information about a domain, it invents concepts, make conjectures, proves theorems and finds counterexamples to false conjectures. We present here a multi-agent version of HR which may provide a model for how individual mathematicians perform separate investigations but communicate their results to the mathematical community, learning from others as they do. We detail the exhaustive categorisation problem to which we have applied a multi-agent approach. |

Steel, Graham; Colton, Simon; Bundy, Alan; Walsh, Toby Cross Domain Mathematical Concept Formation Technical Report The University of Edinburgh 2000. @techreport{steel2000cross, title = {Cross Domain Mathematical Concept Formation}, author = { Graham Steel and Simon Colton and Alan Bundy and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/steel_aisb00.pdf}, year = {2000}, date = {2000-01-01}, institution = {The University of Edinburgh}, abstract = {Many interesting concepts in mathematics are essentially ‘cross-domain’ in nature, relating objects from more than one area of mathematics, e.g. prime order groups. These concepts are often vital to the formation of a mathematical theory. Often, the introduction of cross-domain concepts to an investigation seems to exercise a mathematician’s creative ability. The HR program, (Colton et al., 1999), proposes new concepts in mathematics. Its original implementation was limited to working in one mathematical domain at a time, so it was unable to create cross-domain concepts. Here, we describe an extension of HR to multiple domains. Cross-domain concept formation is facilitated by generalisation of the data structures and heuristic measures employed by the program, and the implementation of a new production rule. Results achieved include generation of the concepts of prime order groups, graph nodes of maximal degree and an interesting class of graph.}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } Many interesting concepts in mathematics are essentially ‘cross-domain’ in nature, relating objects from more than one area of mathematics, e.g. prime order groups. These concepts are often vital to the formation of a mathematical theory. Often, the introduction of cross-domain concepts to an investigation seems to exercise a mathematician’s creative ability. The HR program, (Colton et al., 1999), proposes new concepts in mathematics. Its original implementation was limited to working in one mathematical domain at a time, so it was unable to create cross-domain concepts. Here, we describe an extension of HR to multiple domains. Cross-domain concept formation is facilitated by generalisation of the data structures and heuristic measures employed by the program, and the implementation of a new production rule. Results achieved include generation of the concepts of prime order groups, graph nodes of maximal degree and an interesting class of graph. |

#### 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. @inproceedings{colton2008joined, title = {Joined-Up Reasoning for Automated Scientific Discovery: A Position Statement and Research Agenda}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/FS08-03-004.pdf}, year = {2008}, date = {2008-01-01}, booktitle = {AAAI Fall Symposium: Automated Scientific Discovery}, pages = {18--19}, abstract = {We use the phrase “joined-up” here with a double mean- ing: to convey two aspects of scientific discovery which we believe are essential, yet under-researched with respect to automating scientific discovery processes. Firstly, from an Artificial Intelligence perspective, the majority of ap- proaches to using AI techniques involve a disjointed se- quential application of different problem solving methods, with the user providing the glue in various ways. These in- clude routine logistical aspects such as the pre-processing of data and knowledge, translating outputs into input, choos- ing parameter settings for running AI methods, etc. More importantly, however, the user performs various aspects of meta-level reasoning, including asking the most pertinent questions, determining what it means if a process terminates with success and identifying – and investigating – anoma- lies. This approach tends to lead to auto-assisted discov- eries where the user knows what they are looking for, but not what it looks like, rather than the deeper discoveries of examples/concepts/hypotheses/explanations that the user didn’t even know he or she was looking for. While AI meth- ods promise the discovery of such surprising and novel sci- entific artefacts, they rarely deliver on this promise, as their application is too regimented within the problem solving paradigm of AI.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We use the phrase “joined-up” here with a double mean- ing: to convey two aspects of scientific discovery which we believe are essential, yet under-researched with respect to automating scientific discovery processes. Firstly, from an Artificial Intelligence perspective, the majority of ap- proaches to using AI techniques involve a disjointed se- quential application of different problem solving methods, with the user providing the glue in various ways. These in- clude routine logistical aspects such as the pre-processing of data and knowledge, translating outputs into input, choos- ing parameter settings for running AI methods, etc. More importantly, however, the user performs various aspects of meta-level reasoning, including asking the most pertinent questions, determining what it means if a process terminates with success and identifying – and investigating – anoma- lies. This approach tends to lead to auto-assisted discov- eries where the user knows what they are looking for, but not what it looks like, rather than the deeper discoveries of examples/concepts/hypotheses/explanations that the user didn’t even know he or she was looking for. While AI meth- ods promise the discovery of such surprising and novel sci- entific artefacts, they rarely deliver on this promise, as their application is too regimented within the problem solving paradigm of AI. |

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. @inproceedings{charnley2008global, title = {A Global Workspace Framework for Combining Reasoning Systems}, author = { John Charnley and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/charnley_calculemus08.pdf}, doi = {10.1007/978-3-540-85110-3_21}, isbn = {978-3-540-85110-3}, year = {2008}, date = {2008-01-01}, booktitle = {International Conference on Intelligent Computer Mathematics}, journal = {9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings}, pages = {261--265}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, organization = {Springer}, abstract = {Stand-alone Artificial Intelligence systems for performing specific types of reasoning - such as automated theorem proving and symbolic manipulation in computer algebra systems - are numerous, highly capable and constantly improving. Moreover, systems which combine various forms of reasoning have repeatedly been shown to be more effective than stand-alone systems. For example, the ICARUS system for reformulating constraint satisfaction problems [1] and the HOMER system for conjecture making in number theory [2]. However, in general, such combinations have been ad-hoc in nature and designedwith a specific task in mind. With little general design consideration or a suitable framework for combining reasoning, in general every new combination has to be built from scratch and the resulting system is often inflexible and difficult to manage. We believe it is imperative that generic frameworks are developed if the field of combining reasoning systems is to progress. Such generic frameworkswould provide standardised rule sets and toolkits to simplify the development of combined systems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Stand-alone Artificial Intelligence systems for performing specific types of reasoning - such as automated theorem proving and symbolic manipulation in computer algebra systems - are numerous, highly capable and constantly improving. Moreover, systems which combine various forms of reasoning have repeatedly been shown to be more effective than stand-alone systems. For example, the ICARUS system for reformulating constraint satisfaction problems [1] and the HOMER system for conjecture making in number theory [2]. However, in general, such combinations have been ad-hoc in nature and designedwith a specific task in mind. With little general design consideration or a suitable framework for combining reasoning, in general every new combination has to be built from scratch and the resulting system is often inflexible and difficult to manage. We believe it is imperative that generic frameworks are developed if the field of combining reasoning systems is to progress. Such generic frameworkswould provide standardised rule sets and toolkits to simplify the development of combined systems. |

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. @inproceedings{charnley2008applications, title = {Applications of a Global Workspace Framework to Mathematical Discovery}, author = { John Charnley and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/22874493.pdf}, year = {2008}, date = {2008-01-01}, booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics workshop on Empirically Successful Automated Reasoning for Mathematics}, abstract = {Systems which combine various forms of reasoning such as deductive inference and symbolic manipulation have repeatedly been shown to be more effective than stand-alone systems. In general, however, the combined systems are ad-hoc and designed for a single task. We present a generic framework for combining reasoning processes which is based on the theory of the Global Workspace Architecture. Within this blackboard-style framework, processes attached to a workspace propose information to be broadcast, along with a rating of the importance of the information, and only the most important is broadcast to all the processes, which react accordingly. To begin to demonstrate the value of the framework, we show that the tasks undertaken by previous ad-hoc systems can be performed by a configuration of the framework. To this end, we describe configurations for theorem discovery and conjecture making respectively, which produce comparable results to the previous ICARUS and HOMER systems. We further describe a novel application where we use a configuration of the framework to identify potentially interesting specialisations of finite algebras.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Systems which combine various forms of reasoning such as deductive inference and symbolic manipulation have repeatedly been shown to be more effective than stand-alone systems. In general, however, the combined systems are ad-hoc and designed for a single task. We present a generic framework for combining reasoning processes which is based on the theory of the Global Workspace Architecture. Within this blackboard-style framework, processes attached to a workspace propose information to be broadcast, along with a rating of the importance of the information, and only the most important is broadcast to all the processes, which react accordingly. To begin to demonstrate the value of the framework, we show that the tasks undertaken by previous ad-hoc systems can be performed by a configuration of the framework. To this end, we describe configurations for theorem discovery and conjecture making respectively, which produce comparable results to the previous ICARUS and HOMER systems. We further describe a novel application where we use a configuration of the framework to identify potentially interesting specialisations of finite algebras. |

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. @inproceedings{Sorge2006, title = {Integrating AI Systems for Classification in Non-Associative Algebra}, author = {Volker Sorge and Andreas Meier and Roy McCasland and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/sorge_calculemus06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of the 13th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning }, journal = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, abstract = {The automatic construction of mathematical theorems is a challenging task for Arti-ficial Intelligence systems, which has pushed many research boundaries in different branches of AI. We describe how the construction of classification theorems in algebraic domains of mathematics has driven research not only on the individual mathematical reasoning techniques, but also the integration of these techniques. We have developed a bootstrapping algorithm for the automatic generation of such theorems which relies on the power of model generation, first order theorem proving, computer algebra, machine learning and satisfiability solving. In particular, the con-struction of algebraic invariants demands an intricate interplay of these techniques. We demonstrate the effectiveness of this approach by generating novel theorems which have so far been beyond the reach of automated reasoning systems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The automatic construction of mathematical theorems is a challenging task for Arti-ficial Intelligence systems, which has pushed many research boundaries in different branches of AI. We describe how the construction of classification theorems in algebraic domains of mathematics has driven research not only on the individual mathematical reasoning techniques, but also the integration of these techniques. We have developed a bootstrapping algorithm for the automatic generation of such theorems which relies on the power of model generation, first order theorem proving, computer algebra, machine learning and satisfiability solving. In particular, the con-struction of algebraic invariants demands an intricate interplay of these techniques. We demonstrate the effectiveness of this approach by generating novel theorems which have so far been beyond the reach of automated reasoning systems. |

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. @inproceedings{sorge2004grid, title = {A Grid-based Application of Machine Learning to Model Generation}, author = { Volker Sorge and Simon Colton and Andreas Meier}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/sorge_ki04.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {Poster Proceedings of KI'04}, pages = {204}, abstract = {The classification of mathematical structures is a driving force in pure mathematics. A first step in producing algebraic classification theorems is to de-termine for which sizes certain algebras exist. Computational approaches to solv-ing such existence problems using constraint satisfaction and model generation approaches have had much success. We look here at the question of distributing the model generation process using Grid technology. We present a novel distri-bution approach which involves using the HR machine learning program to intel-ligently suggest specialisations of the problem which are given to separate pro-cessors. Using the MACE, FINDER and SEM model generators, we demonstrate how this approach provides greater efficiency over a single-process approach for a series of quasigroup existence problems. We compare several approaches for the production and choice of specialisations, including the generation of proved classification theorems for algebraic structures of small sizes. We discuss how this approach could be used for more general problems. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The classification of mathematical structures is a driving force in pure mathematics. A first step in producing algebraic classification theorems is to de-termine for which sizes certain algebras exist. Computational approaches to solv-ing such existence problems using constraint satisfaction and model generation approaches have had much success. We look here at the question of distributing the model generation process using Grid technology. We present a novel distri-bution approach which involves using the HR machine learning program to intel-ligently suggest specialisations of the problem which are given to separate pro-cessors. Using the MACE, FINDER and SEM model generators, we demonstrate how this approach provides greater efficiency over a single-process approach for a series of quasigroup existence problems. We compare several approaches for the production and choice of specialisations, including the generation of proved classification theorems for algebraic structures of small sizes. We discuss how this approach could be used for more general problems. |

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. @incollection{meier2002employing, title = {Employing Theory Formation to Guide Proof Planning}, author = { Andreas Meier and Volker Sorge and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/meier_calculemus02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Artificial Intelligence, Automated Reasoning, and Symbolic Computation}, pages = {275--289}, publisher = {Springer}, abstract = {The invention of suitable concepts to characterise mathe-matical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-iso-morphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are gen-erated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system. }, keywords = {}, pubstate = {published}, tppubtype = {incollection} } The invention of suitable concepts to characterise mathe-matical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-iso-morphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are gen-erated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system. |

#### 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. @article{sorge2008automatic, title = {Automatic Construction and Verification of Isotopy Invariants}, author = { Volker Sorge and Andreas Meier and Roy McCasland and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/sorge_jar08.pdf}, year = {2008}, date = {2008-01-01}, journal = {Journal of Automated Reasoning}, volume = {40}, number = {2-3}, pages = {221--243}, publisher = {Springer}, abstract = {We extend our previous study of the automatic construction of iso- morphic classification theorems for algebraic domains by considering the isotopy equivalence relation, which is of more importance than isomorphism in certain domains. This extension was not straightforward, and we had to solve two major technical problems, namely generating and verifying isotopy invariants. Concentrat- ing on the domain of loop theory, we have developed three novel techniques for generating isotopic invariants, by using the notion of universal identities and by using constructions based on sub-blocks. In addition, given the complexity of the theorems which verify that a conjunction of the invariants form an isotopy class, we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an intricate interplay of computer algebra, model generation, theorem proving and satisfiability solving methods. To demonstrate the power of the approach, we generate an isotopic classification theorem for loops of size 6, which extends the previously known result that there are 22. This result was previously beyond the capabilities of automated reasoning techniques.}, keywords = {}, pubstate = {published}, tppubtype = {article} } We extend our previous study of the automatic construction of iso- morphic classification theorems for algebraic domains by considering the isotopy equivalence relation, which is of more importance than isomorphism in certain domains. This extension was not straightforward, and we had to solve two major technical problems, namely generating and verifying isotopy invariants. Concentrat- ing on the domain of loop theory, we have developed three novel techniques for generating isotopic invariants, by using the notion of universal identities and by using constructions based on sub-blocks. In addition, given the complexity of the theorems which verify that a conjunction of the invariants form an isotopy class, we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an intricate interplay of computer algebra, model generation, theorem proving and satisfiability solving methods. To demonstrate the power of the approach, we generate an isotopic classification theorem for loops of size 6, which extends the previously known result that there are 22. This result was previously beyond the capabilities of automated reasoning techniques. |

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. @article{sorge2008classification, title = {Classification Results in Quasigroup and Loop Theory via a Combination of Automated Reasoning Tools}, author = { Volker Sorge and Simon Colton and Roy McCasland and Andreas Meier}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/sorge_carolinae08.pdf}, year = {2008}, date = {2008-01-01}, journal = {Commentationes Mathematicae Universitatis Carolinae}, volume = {49}, number = {2}, pages = {319--340}, publisher = {Prague [Mathematical Institute of the Charles University]}, abstract = {Abstract. We present some novel partial classification results in quasigroup and loop theory. For quasigroups up to size XXX and loops up to size YYY, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques – including machine learning and computer algebra – which we present here. Moreover, each result has been automatically verified, again using a variety of techniques – including automated theorem proving, computer algebra and satisfiability solving – and we describe our bootstrapping approach to the generation and verification of these classification results.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Abstract. We present some novel partial classification results in quasigroup and loop theory. For quasigroups up to size XXX and loops up to size YYY, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques – including machine learning and computer algebra – which we present here. Moreover, each result has been automatically verified, again using a variety of techniques – including automated theorem proving, computer algebra and satisfiability solving – and we describe our bootstrapping approach to the generation and verification of these classification results. |

Colton, Simon; Sorge, Volker Automated Parameterisation of Finite Algebras Inproceedings In: Workshop on Empirical Successful Automated Reasoning in Mathematics, 2008. @inproceedings{colton2008automated, title = {Automated Parameterisation of Finite Algebras}, author = { Simon Colton and Volker Sorge}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_esarm08.pdf}, year = {2008}, date = {2008-01-01}, booktitle = {Workshop on Empirical Successful Automated Reasoning in Mathematics}, abstract = {In previous work we have designed an automatic bootstrap- ping algorithm to classify finite algebraic structures by generating prop- erties that uniquely describe and discriminate different equivalence classes. One of the drawbacks of the approach was that during the classification a large number different discriminating properties were generated. This made it particularly difficult to compare classifying properties for dif- ferent sizes of algebraic structures. To minimise the overall number of properties needed we have now experimented with parameterising struc- tures by counting the number of elements with particular properties. Isomorphism classes are then discriminated by the different number of elements with the same property. With this new approach we can now classify large numbers of algebraic structures using only a small number of properties. We were able to construct and prove parameterisations for algebraic structures like loops of size 6 and groups of size 8. However, the approach is currently limited as translating counting arguments into pure first order or propositional logic, often makes for prohibitively long problem formulations. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In previous work we have designed an automatic bootstrap- ping algorithm to classify finite algebraic structures by generating prop- erties that uniquely describe and discriminate different equivalence classes. One of the drawbacks of the approach was that during the classification a large number different discriminating properties were generated. This made it particularly difficult to compare classifying properties for dif- ferent sizes of algebraic structures. To minimise the overall number of properties needed we have now experimented with parameterising struc- tures by counting the number of elements with particular properties. Isomorphism classes are then discriminated by the different number of elements with the same property. With this new approach we can now classify large numbers of algebraic structures using only a small number of properties. We were able to construct and prove parameterisations for algebraic structures like loops of size 6 and groups of size 8. However, the approach is currently limited as translating counting arguments into pure first order or propositional logic, often makes for prohibitively long problem formulations. |

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. @inbook{colton2007computational, title = {Computational Discovery in Pure Mathematics}, author = { Simon Colton}, editor = {Saso Dzeroski and Ljupco Todorowski}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_cdck07.pdf}, year = {2007}, date = {2007-01-01}, booktitle = {Computational Discovery of Scientific Knowledge}, journal = {Communicable Scientific Discovery, LNAI}, volume = {4660}, pages = {175--201}, publisher = {Springer}, abstract = {We discuss what constitutes knowledge in pure mathemat- ics and how new advances are made and communicated. We describe the impact of computer algebra systems, automated theorem provers, programs designed to generate examples, mathematical databases, and theory formation programs on the body of knowledge in pure mathemat- ics. We discuss to what extent the output from certain programs can be considered a discovery in pure mathematics. This enables us to assess the state of the art with respect to Newell and Simon’s prediction that a computer would discover and prove an important mathematical theorem.}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } We discuss what constitutes knowledge in pure mathemat- ics and how new advances are made and communicated. We describe the impact of computer algebra systems, automated theorem provers, programs designed to generate examples, mathematical databases, and theory formation programs on the body of knowledge in pure mathemat- ics. We discuss to what extent the output from certain programs can be considered a discovery in pure mathematics. This enables us to assess the state of the art with respect to Newell and Simon’s prediction that a computer would discover and prove an important mathematical theorem. |

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. @article{colton2005automated, title = {Automated Conjecture Making In Number Theory Using HR, Otter and Maple}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_jsc05.pdf}, year = {2005}, date = {2005-01-01}, journal = {Journal of Symbolic Computation}, volume = {39}, number = {5}, pages = {593--615}, publisher = {Elsevier}, abstract = {One of the main applications of computational techniques to pure math- ematics has been the use of computer algebra systems to perform cal- culations which mathematicians cannot perform by hand. Because the data is produced within the computer algebra system, this becomes an environment for the exploration of new functions and the data produced is often analysed in order to make conjectures empirically. We add some automation to this discovery process by using the HR theory formation system to make conjectures about Maple functions supplied by the user. HR forms theories by inventing concepts, making conjectures empirically which relate the concepts, and appealing to third party theorem provers and model generators to prove/disprove the conjectures. It has been used with success in number theory, graph theory and various algebraic do- mains such as group theory and ring theory. Experience has shown that HR produces too many conjectures which can be easily proven from the definitions of the functions involved. Hence, we use the Otter theorem prover to discard any theorems which can be easily proven, leaving behind the more interesting ones which are empiri- cally plausible but not easily provable. We describe the core functionality of HR which enables it to form a theory, and the additional functionality implemented in order for HR to work with Maple functions. We present two experiments where we have applied HR’s theory formation in number theory. We discuss the modes of operation for the user and provide some of the results produced in this way. We hope to show that using HR, Ot- ter and Maple in this fashion has much potential for the advancement of computer algebra systems.}, keywords = {}, pubstate = {published}, tppubtype = {article} } One of the main applications of computational techniques to pure math- ematics has been the use of computer algebra systems to perform cal- culations which mathematicians cannot perform by hand. Because the data is produced within the computer algebra system, this becomes an environment for the exploration of new functions and the data produced is often analysed in order to make conjectures empirically. We add some automation to this discovery process by using the HR theory formation system to make conjectures about Maple functions supplied by the user. HR forms theories by inventing concepts, making conjectures empirically which relate the concepts, and appealing to third party theorem provers and model generators to prove/disprove the conjectures. It has been used with success in number theory, graph theory and various algebraic do- mains such as group theory and ring theory. Experience has shown that HR produces too many conjectures which can be easily proven from the definitions of the functions involved. Hence, we use the Otter theorem prover to discard any theorems which can be easily proven, leaving behind the more interesting ones which are empiri- cally plausible but not easily provable. We describe the core functionality of HR which enables it to form a theory, and the additional functionality implemented in order for HR to work with Maple functions. We present two experiments where we have applied HR’s theory formation in number theory. We discuss the modes of operation for the user and provide some of the results produced in this way. We hope to show that using HR, Ot- ter and Maple in this fashion has much potential for the advancement of computer algebra systems. |

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. @inproceedings{colton2004automatic, title = {Automatic Generation of Classification Theorems for Finite Algebras}, author = { Simon Colton and Andreas Meier and Volker Sorge and Roy McCasland}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ijcar04.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {International Joint Conference on Automated Reasoning}, pages = {400--414}, organization = {Springer}, abstract = {Classifying finite algebraic structures has been a major mo- tivation behind much research in pure mathematics. Automated tech- niques have aided in this process, but this has largely been at a quan- titative level. In contrast, we present a qualitative approach which pro- duces verified theorems, which classify algebras of a particular type and size into isomorphism classes. We describe both a semi-automated and a fully automated bootstrapping approach to building and verifying clas- sification theorems. In the latter case, we have implemented a procedure which takes the axioms of the algebra and produces a decision tree em- bedding a fully verified classification theorem. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the Mace model generator, the HR and C4.5 machine learning systems, the Spass theorem prover, and the Gap computer al- gebra system to reduce the complexity of the problems given to Spass. We demonstrate the power of this approach by classifying loops, groups, monoids and quasigroups of various sizes.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Classifying finite algebraic structures has been a major mo- tivation behind much research in pure mathematics. Automated tech- niques have aided in this process, but this has largely been at a quan- titative level. In contrast, we present a qualitative approach which pro- duces verified theorems, which classify algebras of a particular type and size into isomorphism classes. We describe both a semi-automated and a fully automated bootstrapping approach to building and verifying clas- sification theorems. In the latter case, we have implemented a procedure which takes the axioms of the algebra and produces a decision tree em- bedding a fully verified classification theorem. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the Mace model generator, the HR and C4.5 machine learning systems, the Spass theorem prover, and the Gap computer al- gebra system to reduce the complexity of the problems given to Spass. We demonstrate the power of this approach by classifying loops, groups, monoids and quasigroups of various sizes. |

Colton, Simon; Muggleton, Stephen ILP for Mathematical Discovery Inproceedings In: International Conference on Inductive Logic Programming, pp. 93–111, Springer 2003. @inproceedings{colton2003ilp, title = {ILP for Mathematical Discovery}, author = { Simon Colton and Stephen Muggleton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ilp03.pdf}, year = {2003}, date = {2003-01-01}, booktitle = {International Conference on Inductive Logic Programming}, pages = {93--111}, organization = {Springer}, abstract = {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 describe the HR system which performs a novel ILP routine called automated the- ory formation. This 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 defi- nitions 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 to a range of predictive, descriptive and subgroup discovery tasks in domains of pure mathematics. We describe these applications and how they have led to some interesting mathematical discoveries. Our main aim here is to provide a thorough overview of automated theory for- mation. A secondary aim is to promote mathematics as a worthy domain for ILP applications, and we provide pointers to mathematical datasets.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } 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 describe the HR system which performs a novel ILP routine called automated the- ory formation. This 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 defi- nitions 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 to a range of predictive, descriptive and subgroup discovery tasks in domains of pure mathematics. We describe these applications and how they have led to some interesting mathematical discoveries. Our main aim here is to provide a thorough overview of automated theory for- mation. A secondary aim is to promote mathematics as a worthy domain for ILP applications, and we provide pointers to mathematical datasets. |

Colton, Simon; Huczynska, Sophie The HOMER System Inproceedings In: International Conference on Automated Deduction, pp. 289–294, Springer 2003. @inproceedings{colton2003homer, title = {The HOMER System}, author = { Simon Colton and Sophie Huczynska}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_cade03.pdf}, year = {2003}, date = {2003-01-01}, booktitle = {International Conference on Automated Deduction}, pages = {289--294}, organization = {Springer}, abstract = {The Homer system combines the HR automated theory formation program, the Otter theorem prover, and the Maple computer algebra package [1] to make intelligent conjectures about number theory functions supplied by the user. The integration is as follows: given Maple code for some functions the user is in-terested in, Maple is used to calculate values for those functions. HR then forms a theory using the functions as background knowledge, calling Maple when-ever necessary to perform additional calculations. The theory formation process makes conjectures empirically and the user is initially asked to prove or disprove each conjecture. As the theory formation progresses, however, Homer uses the theorems it has found (namely those proved by the user) as axioms in attempts to prove the conjectures itself using Otter. Any conjectures proved in this way are likely to follow easily from the theorems already known to the user, so Homer does not present them, in order to keep the quality of the output high. Using Otter in this extreme way is not meant to indicate that Otter can only prove trivial theorems, nor that HR produces too many dull conjectures. Rather, we wish to emphasise the power of the combined system (Homer) at discovering interesting conjectures by generate (HR) and quick test (Otter). }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The Homer system combines the HR automated theory formation program, the Otter theorem prover, and the Maple computer algebra package [1] to make intelligent conjectures about number theory functions supplied by the user. The integration is as follows: given Maple code for some functions the user is in-terested in, Maple is used to calculate values for those functions. HR then forms a theory using the functions as background knowledge, calling Maple when-ever necessary to perform additional calculations. The theory formation process makes conjectures empirically and the user is initially asked to prove or disprove each conjecture. As the theory formation progresses, however, Homer uses the theorems it has found (namely those proved by the user) as axioms in attempts to prove the conjectures itself using Otter. Any conjectures proved in this way are likely to follow easily from the theorems already known to the user, so Homer does not present them, in order to keep the quality of the output high. Using Otter in this extreme way is not meant to indicate that Otter can only prove trivial theorems, nor that HR produces too many dull conjectures. Rather, we wish to emphasise the power of the combined system (Homer) at discovering interesting conjectures by generate (HR) and quick test (Otter). |

Colton, Simon Making Conjectures About Maple Functions Incollection In: Artificial Intelligence, Automated Reasoning, and Symbolic Computation, pp. 259–274, Springer, 2002. @incollection{colton2002making, title = {Making Conjectures About Maple Functions}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_calculemus02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Artificial Intelligence, Automated Reasoning, and Symbolic Computation}, pages = {259--274}, publisher = {Springer}, abstract = {One of the main applications of computational techniques to pure mathematics has been the use of computer algebra systems to perform calculations which mathematicians cannot perform by hand. Because the data is produced within the computer algebra system, this becomes an environment for the exploration of new functions and the data produced is often analysed in order to make conjectures empirically. We add some automation to this by using the HR theory formation system to make conjectures about Maple functions supplied by the user. Experience has shown that HR produces too many conjectures which are easily proven from the definitions of the functions involved. Hence, we use the Otter theorem prover to discard any theorems which can be easily proven, leaving behind the more interesting ones which are empirically true but not trivially provable. By providing an application of HR's theory formation in number theory, we show that using Otter to prune HR's dull conjectures has much potential for producing interesting conjectures about standard computer algebra functions. }, keywords = {}, pubstate = {published}, tppubtype = {incollection} } One of the main applications of computational techniques to pure mathematics has been the use of computer algebra systems to perform calculations which mathematicians cannot perform by hand. Because the data is produced within the computer algebra system, this becomes an environment for the exploration of new functions and the data produced is often analysed in order to make conjectures empirically. We add some automation to this by using the HR theory formation system to make conjectures about Maple functions supplied by the user. Experience has shown that HR produces too many conjectures which are easily proven from the definitions of the functions involved. Hence, we use the Otter theorem prover to discard any theorems which can be easily proven, leaving behind the more interesting ones which are empirically true but not trivially provable. By providing an application of HR's theory formation in number theory, we show that using Otter to prune HR's dull conjectures has much potential for producing interesting conjectures about standard computer algebra functions. |

Colton, Simon; Dennis, Louise Abigail The NumbersWithNames Program Inproceedings In: Proceedings of the Seventh AI and Maths Symposium, 2002. @inproceedings{colton2002numberswithnames, title = {The NumbersWithNames Program}, author = { Simon Colton and Louise Abigail Dennis}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aim02_1.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Proceedings of the Seventh AI and Maths Symposium}, abstract = {We present the NumbersWithNames program which performs data-mining on the Encyclopedia of Integer Sequences to find interesting conjectures in number theory. The program forms conjec-tures by finding empirical relationships between a sequence chosen by the user and those in the Encyclopedia. Furthermore, it transforms the chosen sequence into another set of sequences about which conjectures can also be formed. Finally, the program prunes and sorts the conjectures so that the most plausible ones are presented first. We describe here the many improvements to the previous Prolog implementation which have enabled us to provide NumbersWithNames as an online program. We also present some new results from using NumbersWithNames, including details of an automated proof plan of a conjecture NumbersWithNames helped to discover. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We present the NumbersWithNames program which performs data-mining on the Encyclopedia of Integer Sequences to find interesting conjectures in number theory. The program forms conjec-tures by finding empirical relationships between a sequence chosen by the user and those in the Encyclopedia. Furthermore, it transforms the chosen sequence into another set of sequences about which conjectures can also be formed. Finally, the program prunes and sorts the conjectures so that the most plausible ones are presented first. We describe here the many improvements to the previous Prolog implementation which have enabled us to provide NumbersWithNames as an online program. We also present some new results from using NumbersWithNames, including details of an automated proof plan of a conjecture NumbersWithNames helped to discover. |

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. @inproceedings{colton2002automated, title = {Automated Theory Formation for Tutoring Tasks in Pure Mathematics}, author = { Simon Colton and Roy McCasland and Alan Bundy and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_radm02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {In CADE-18, Workshop on the Role of Automated Deduction in Mathematics}, organization = {Citeseer}, abstract = {The HR program forms mathematical theories from as little infor-mation as the axioms of a domain. The theories include concepts with examples and definitions, conjectures, theorems and proofs. Moreover, HR uses third party mathematical software including automated theorem provers and model generators. We suggest that a potential role for theory formation systems such as HR is as an aid to mathematics lecturers. We discuss an application of HR to the generation of a set of group theory exercises. This forms part of a project using HR to make discoveries in Zariski spaces, which is also detailed. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The HR program forms mathematical theories from as little infor-mation as the axioms of a domain. The theories include concepts with examples and definitions, conjectures, theorems and proofs. Moreover, HR uses third party mathematical software including automated theorem provers and model generators. We suggest that a potential role for theory formation systems such as HR is as an aid to mathematics lecturers. We discuss an application of HR to the generation of a set of group theory exercises. This forms part of a project using HR to make discoveries in Zariski spaces, which is also detailed. |

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. @inproceedings{bundysemi, title = {Semi-Automated Discovery in Zariski Spaces (A Proposal)}, author = { Alan Bundy and Simon Colton and Roy McCasland and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/bundy_arw02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, journal = {Automated Reasoning Workshop}, abstract = {Zariski Spaces were introduced in 1998 [MMS98]. In order to understand these spaces, one needs to first understand Zariski Topologies. In a broad sense, these topologies are rather like prime factorizations. For example, the Zariski topology associated with the ring of integers consists of sets (called varieties) of prime ideals, one set for each integer. In particular, the variety of the integer 12 would be the set of ideals generated by 2 and by 3, respectively, since 2 and 3 are the prime factors of 12. Note that since 2 and 3 both divide 12, then the ideal generated by 2 and the ideal generated by 3 both contain the ideal generated by 12. In the general case, let R be a commutative ring with unity, and let specR denote the collection of prime ideals of R.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Zariski Spaces were introduced in 1998 [MMS98]. In order to understand these spaces, one needs to first understand Zariski Topologies. In a broad sense, these topologies are rather like prime factorizations. For example, the Zariski topology associated with the ring of integers consists of sets (called varieties) of prime ideals, one set for each integer. In particular, the variety of the integer 12 would be the set of ideals generated by 2 and by 3, respectively, since 2 and 3 are the prime factors of 12. Note that since 2 and 3 both divide 12, then the ideal generated by 2 and the ideal generated by 3 both contain the ideal generated by 12. In the general case, let R be a commutative ring with unity, and let specR denote the collection of prime ideals of R. |

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. @inproceedings{Colton2001, title = {Mathematics - a new Domain for Datamining?}, author = {Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ijcai01.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {Proceedings of the IJCAI-01 Workshop on Knowledge Discovery from Distributed, Dynamic, Heterogenous, Autonomous Sources}, journal = {International Joint Conference on Artificial Intelligence}, abstract = {With the many databases of mathematical informa-tion currently available, there is much potential for datamining techniques to find new and interesting mathematical results. Indeed, we suggest that, if we can utilise the research into dealing with dynamic, dis-tributed and heterogeneous datasets, datamining could be as successful a technique for mathematics as it is for, say, biology. We briefly survey 7 mathematical databases available online and present a motivating example and a case study. This enables us to high-light important issues and to make some suggestions for datamining mathematical information. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } With the many databases of mathematical informa-tion currently available, there is much potential for datamining techniques to find new and interesting mathematical results. Indeed, we suggest that, if we can utilise the research into dealing with dynamic, dis-tributed and heterogeneous datasets, datamining could be as successful a technique for mathematics as it is for, say, biology. We briefly survey 7 mathematical databases available online and present a motivating example and a case study. This enables us to high-light important issues and to make some suggestions for datamining mathematical information. |

Colton, Simon; Bundy, Alan; Walsh, Toby Automatic Invention of Integer Sequences Inproceedings In: AAAI/IAAI, pp. 558–563, 2000. @inproceedings{colton2000automaticb, title = {Automatic Invention of Integer Sequences}, author = { Simon Colton and Alan Bundy and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aaai00.pdf}, year = {2000}, date = {2000-01-01}, booktitle = {AAAI/IAAI}, pages = {558--563}, abstract = {We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically in- venting integer sequences. Seventeen sequences invented by HR are interesting enough to have been accepted into the En- cyclopedia of Integer Sequences (Sloane 2000) and all were supplied with interesting conjectures about their nature, also discovered by HR. By extending HR, we have enabled it to perform a two stage process of invention and investigation. This involves generating both the definition and terms of a new sequence, relating it to sequences already in the Encyc- lopedia and pruning the output to help identify the most sur- prising and interesting results. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically in- venting integer sequences. Seventeen sequences invented by HR are interesting enough to have been accepted into the En- cyclopedia of Integer Sequences (Sloane 2000) and all were supplied with interesting conjectures about their nature, also discovered by HR. By extending HR, we have enabled it to perform a two stage process of invention and investigation. This involves generating both the definition and terms of a new sequence, relating it to sequences already in the Encyc- lopedia and pruning the output to help identify the most sur- prising and interesting results. |

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. @article{colton2000notion, title = {On the Notion of Interestingness in Automated Mathematical Discovery}, author = { Simon Colton and Alan Bundy and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ijhcs00.pdf}, year = {2000}, date = {2000-01-01}, journal = {International Journal of Human-Computer Studies}, volume = {53}, number = {3}, pages = {351--375}, publisher = {Elsevier}, abstract = {We survey five mathematical discovery programs by looking in detail at the discovery processes they illustrate and the success they’ve had. We focus on how they estimate the interestingness of concepts and conjectures and extract some common notions about interestingness in automated mathematical discovery. We detail how empirical evidence is used to give plausibility to conjectures, and the different ways in which a result can be thought of as novel. We also look at the ways in which the programs assess how surprising and complex a conjecture statement is, and the different ways in which the applicability of a concept or conjecture is used. Finally, we note how a user can set tasks for the program to achieve and how this affects the calculation of interestingness. We conclude with some hints on the use of interestingness measures for future developers of discovery programs in mathematics.}, keywords = {}, pubstate = {published}, tppubtype = {article} } We survey five mathematical discovery programs by looking in detail at the discovery processes they illustrate and the success they’ve had. We focus on how they estimate the interestingness of concepts and conjectures and extract some common notions about interestingness in automated mathematical discovery. We detail how empirical evidence is used to give plausibility to conjectures, and the different ways in which a result can be thought of as novel. We also look at the ways in which the programs assess how surprising and complex a conjecture statement is, and the different ways in which the applicability of a concept or conjecture is used. Finally, we note how a user can set tasks for the program to achieve and how this affects the calculation of interestingness. We conclude with some hints on the use of interestingness measures for future developers of discovery programs in mathematics. |

Colton, Simon; Bundy, Alan; Walsh, Toby Automated Discovery in Pure Mathematics Inproceedings In: Automated Reasoning Workshop: Bridging the Gap between Theory and Practice, 1999. @inproceedings{colton1999automated, title = {Automated Discovery in Pure Mathematics}, author = { Simon Colton and Alan Bundy and Toby Walsh}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_arw99.pdf}, year = {1999}, date = {1999-01-01}, booktitle = {Automated Reasoning Workshop: Bridging the Gap between Theory and Practice}, abstract = {The HR project aims to automate two important discovery processes which occur in mathematics before theorem proving happens, namely the making of the conjecture to be proved and the invention of the definitions in the conjecture statement.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The HR project aims to automate two important discovery processes which occur in mathematics before theorem proving happens, namely the making of the conjecture to be proved and the invention of the definitions in the conjecture statement. |

Colton, Simon Refactorable numbers-a machine invention Journal Article In: Journal of Integer Sequences, 2 (99.1), pp. 2, 1999. @article{colton1999refactorable, title = {Refactorable numbers-a machine invention}, author = { Simon Colton}, url = {http://emis.ams.org/journals/JIS/colton/joisol.html}, year = {1999}, date = {1999-01-01}, journal = {Journal of Integer Sequences}, volume = {2}, number = {99.1}, pages = {2}, keywords = {}, pubstate = {published}, tppubtype = {article} } |

#### 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. @inproceedings{colton2014countdown, title = {Countdown Numbers Game: Solved, Analysed, Extended}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aisb14a.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the AISB symposium on AI and Games}, abstract = {The Countdown Numbers Game is a popular arithmeti- cal puzzle which has been played as a two-player game on French and British television weekly for decades. We have solved this game in the sense that the optimal solution for the nearly 12 million puzzle instances has been generated and recorded. We describe here how we have achieved this using the HR3 Automated Theory Formation system. This has allowed us to analyse the space of puzzles; sug- gest gamesmanship tactics and game design improvements to the online/handheld versions of the game; and begin to investigate the potential for automatic invention of such games.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The Countdown Numbers Game is a popular arithmeti- cal puzzle which has been played as a two-player game on French and British television weekly for decades. We have solved this game in the sense that the optimal solution for the nearly 12 million puzzle instances has been generated and recorded. We describe here how we have achieved this using the HR3 Automated Theory Formation system. This has allowed us to analyse the space of puzzles; sug- gest gamesmanship tactics and game design improvements to the online/handheld versions of the game; and begin to investigate the potential for automatic invention of such games. |

Grov, Gudmund; Farquhar, Colin; Pease, Alison; Colton, Simon Tinkering by Theory Formation Inproceedings In: Proceedings of the AIFM workshop, 2014. @inproceedings{grov2014tinkering, title = {Tinkering by Theory Formation}, author = { Gudmund Grov and Colin Farquhar and Alison Pease and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/grov_AIFM14.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the AIFM workshop}, abstract = {Most interactive theorem provers support encoding of common proof strategies as special func- tion called tactics. Such tactics tend to work backwards from the goal, reducing a goal to a set of simpler sub-goals. Proof strategies are then created by combining such tactics using a tactic language. Such languages are often not designed to distinguish goals in cases where tactics produce multiple sub-goals. Thus when composing tactics, one has no choice but to rely on the order in which goals arrive, thus making them brittle to minor changes. For example, consider a case where we expect three sub-goals from tactic t1, where the first two are sent to t2 and the last to t3. A small improvement of t1 may result in only two sub-goals. This “improvement” causes t2 to be applied to the second goal when it should have been t3. The tactic t2 may then fail or create unexpected new sub-goals that cause some later tactic to fail.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Most interactive theorem provers support encoding of common proof strategies as special func- tion called tactics. Such tactics tend to work backwards from the goal, reducing a goal to a set of simpler sub-goals. Proof strategies are then created by combining such tactics using a tactic language. Such languages are often not designed to distinguish goals in cases where tactics produce multiple sub-goals. Thus when composing tactics, one has no choice but to rely on the order in which goals arrive, thus making them brittle to minor changes. For example, consider a case where we expect three sub-goals from tactic t1, where the first two are sent to t2 and the last to t3. A small improvement of t1 may result in only two sub-goals. This “improvement” causes t2 to be applied to the second goal when it should have been t3. The tactic t2 may then fail or create unexpected new sub-goals that cause some later tactic to fail. |

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. @inproceedings{cavallo2013using, title = {Using Theory Formation Techniques for the Invention of Fictional Concepts}, author = { Flaminia Cavallo and Alison Pease and Jeremy Gow and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/cavallo_iccc13.pdf}, year = {2013}, date = {2013-01-01}, booktitle = {Proceedings of the Fourth International Conference on Computational Creativity}, pages = {176}, abstract = {We introduce a novel method for the formation of fictional concepts based on the non-existence conjectures made by the HR automated theory formation system. We further intro- duce the notion of the typicality of an example with respect to a concept into HR, which leads to methods for ordering fic- tional concepts with respect to novelty, vagueness and stimu- lation. To test whether these measures are correlated with the way in which people similarly assess the value of fictional concepts, we ran an experiment to produce thousands of defi- nitions of fictional animals. We then compared the software’s evaluations of the non-fictional concepts with those obtained through a survey consulting sixty people. The results show that two of the three measures have a correlation with hu- man notions. We report on the experiment, and we compare our system with the well established method of conceptual blending, which leads to a discussion of automated ideation in future Computational Creativity projects.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We introduce a novel method for the formation of fictional concepts based on the non-existence conjectures made by the HR automated theory formation system. We further intro- duce the notion of the typicality of an example with respect to a concept into HR, which leads to methods for ordering fic- tional concepts with respect to novelty, vagueness and stimu- lation. To test whether these measures are correlated with the way in which people similarly assess the value of fictional concepts, we ran an experiment to produce thousands of defi- nitions of fictional animals. We then compared the software’s evaluations of the non-fictional concepts with those obtained through a survey consulting sixty people. The results show that two of the three measures have a correlation with hu- man notions. We report on the experiment, and we compare our system with the well established method of conceptual blending, which leads to a discussion of automated ideation in future Computational Creativity projects. |

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. @inproceedings{llano2011using, title = {Using Automated Theory Formation to Discover Invariants of Event-B Models}, author = { Maria Teresa Llano and Andrew Ireland and Alison Pease and Simon Colton and John Charnley}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/llano_rodin10.pdf}, year = {2010}, date = {2010-01-01}, booktitle = {In Proceedings of the Rodin User and Developer Workshop}, abstract = {Formal methods have been successfully used for the development of safety-critical systems; however, the need for skilled knowledge when writing formal models and reasoning about them represents a major barrier in the adoption of formal methodologies for the development of non-critical applications. A key aspect in the verification of formal models and in the development of reliable systems is the identification of invariants. However, finding correct and meaningful invariants for a model represents a significant challenge. We have used automated theory formation (ATF) techniques to automatically discover invariants of Event-B models. In particular, we use Colton’s HR system [2] to explore the domain of Event-B models and suggest potential invariants.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Formal methods have been successfully used for the development of safety-critical systems; however, the need for skilled knowledge when writing formal models and reasoning about them represents a major barrier in the adoption of formal methodologies for the development of non-critical applications. A key aspect in the verification of formal models and in the development of reliable systems is the identification of invariants. However, finding correct and meaningful invariants for a model represents a significant challenge. We have used automated theory formation (ATF) techniques to automatically discover invariants of Event-B models. In particular, we use Colton’s HR system [2] to explore the domain of Event-B models and suggest potential invariants. |

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. @inproceedings{baumgarten2009towards, title = {Towards the Automatic Invention of Simple Mixed Reality Games}, author = { Robin Baumgarten and Maria Nika and Jeremy Gow and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_evomusart08.pdf}, year = {2009}, date = {2009-01-01}, booktitle = {Proc. of the AISB’09 Symp. on AI and Games}, abstract = {We investigate the automatic construction of visual scenes via a hybrid evolutionary/hill-climbing approach using a correlation- based fitness function. This forms part of The Painting Fool system, an automated artist which is able to render the scenes using simulated art materials. We further describe a novel method for inventing fitness functions using the HR descriptive machine learning system, and we com- bine this with The Painting Fool to generate and artistically render novel scenes. We demonstrate the potential of this approach with applications to cityscape and flower arrangement scene generation.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We investigate the automatic construction of visual scenes via a hybrid evolutionary/hill-climbing approach using a correlation- based fitness function. This forms part of The Painting Fool system, an automated artist which is able to render the scenes using simulated art materials. We further describe a novel method for inventing fitness functions using the HR descriptive machine learning system, and we com- bine this with The Painting Fool to generate and artistically render novel scenes. We demonstrate the potential of this approach with applications to cityscape and flower arrangement scene generation. |

Colton, Simon Automatic Invention of Fitness Functions, with application to Scene Generation Inproceedings In: Proceedings of the EvoMusArt Workshop, 2008. @inproceedings{Colton2008EvoMusArt, title = {Automatic Invention of Fitness Functions, with application to Scene Generation}, author = {Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/11/colton_evomusart08.pdf}, year = {2008}, date = {2008-11-01}, booktitle = {Proceedings of the EvoMusArt Workshop}, abstract = {We investigate the automatic construction of visual scenes via a hybrid evolutionary/hill-climbing approach using a correlation- based fitness function. This forms part of The Painting Fool system, an automated artist which is able to render the scenes using simulated art materials. We further describe a novel method for inventing fitness functions using the HR descriptive machine learning system, and we com- bine this with The Painting Fool to generate and artistically render novel scenes. We demonstrate the potential of this approach with applications to cityscape and flower arrangement scene generation. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We investigate the automatic construction of visual scenes via a hybrid evolutionary/hill-climbing approach using a correlation- based fitness function. This forms part of The Painting Fool system, an automated artist which is able to render the scenes using simulated art materials. We further describe a novel method for inventing fitness functions using the HR descriptive machine learning system, and we com- bine this with The Painting Fool to generate and artistically render novel scenes. We demonstrate the potential of this approach with applications to cityscape and flower arrangement scene generation. |

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. @inproceedings{jiang2006boosting, title = {Boosting Descriptive ILP for Predictive Learning in Bioinformatics}, author = { Ning Jiang and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/jiang_ilp06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {International Conference on Inductive Logic Programming}, pages = {275--289}, organization = {Springer}, abstract = {Boosting is an established propositional learning method to promote the predictive accuracy of weak learning algorithms, and has achieved much empirical success. However, there have been relatively few efforts to apply boosting to Inductive Logic Programming (ILP) ap- proaches. We investigate the use of boosting descriptive ILP systems, by proposing a novel algorithm for generating classification rules which searches using a hybrid language bias/production rule approach, and a new method for converting first-order classification rules to binary clas- sifiers, which increases the predictive accuracy of the boosted classifiers. We demonstrate that our boosted approach is competitive with normal ILP systems in experiments with bioinformatics datasets.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Boosting is an established propositional learning method to promote the predictive accuracy of weak learning algorithms, and has achieved much empirical success. However, there have been relatively few efforts to apply boosting to Inductive Logic Programming (ILP) ap- proaches. We investigate the use of boosting descriptive ILP systems, by proposing a novel algorithm for generating classification rules which searches using a hybrid language bias/production rule approach, and a new method for converting first-order classification rules to binary clas- sifiers, which increases the predictive accuracy of the boosted classifiers. We demonstrate that our boosted approach is competitive with normal ILP systems in experiments with bioinformatics datasets. |

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. @incollection{santos2006predictive, title = {Predictive and Descriptive Approaches to Learning Game Rules from Vision Data}, author = { Paulo Santos and Simon Colton and Derek Magee}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/santos_iberamia06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Advances in Artificial Intelligence-IBERAMIA-SBIA 2006}, pages = {349--359}, publisher = {Springer}, abstract = {Systems able to learn from visual observations have a great deal of potential for autonomous robotics, scientific discovery, and many other fields as the necessity to generalise from visual observation (from a quotidian scene or from the results of a scientific enquiry) is inherent in various domains. We de- scribe an application to learning rules of a dice game using data from a vision system observing the game being played. In this paper, we experimented with two broad approaches: (i) a predictive learning approach with the Progol system, where explicit concept learning problems are posed and solved, and (ii) a descrip- tive learning approach with the HR system, where a general theory is formed with no specific problem solving task in mind and rules are extracted from the theory.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } Systems able to learn from visual observations have a great deal of potential for autonomous robotics, scientific discovery, and many other fields as the necessity to generalise from visual observation (from a quotidian scene or from the results of a scientific enquiry) is inherent in various domains. We de- scribe an application to learning rules of a dice game using data from a vision system observing the game being played. In this paper, we experimented with two broad approaches: (i) a predictive learning approach with the Progol system, where explicit concept learning problems are posed and solved, and (ii) a descrip- tive learning approach with the HR system, where a general theory is formed with no specific problem solving task in mind and rules are extracted from the theory. |

Colton, Simon Automated Puzzle Generation Inproceedings In: Proceedings of the AISB’02 Symposium on AI and Creativity in the Arts and Science, 2002. @inproceedings{colton2002automatedb, title = {Automated Puzzle Generation}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aisb02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Proceedings of the AISB’02 Symposium on AI and Creativity in the Arts and Science}, abstract = {We give a characterisation of certain types of puzzle in terms of the structure of the question posed and the nature of the answer to the puzzle. Using this characterisation, we have extended the HR theory formation system (2) to enable it to automatically generate puzzles given background information about a set of objects of interest. The main technical difficulty to overcome was to ensure that the puzzles generated by HR had a single solution (up to a level of plausibility). We give details of the implementation and some results from its application.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We give a characterisation of certain types of puzzle in terms of the structure of the question posed and the nature of the answer to the puzzle. Using this characterisation, we have extended the HR theory formation system (2) to enable it to automatically generate puzzles given background information about a set of objects of interest. The main technical difficulty to overcome was to ensure that the puzzles generated by HR had a single solution (up to a level of plausibility). We give details of the implementation and some results from its application. |

Colton, Simon Automated Theory Formation Applied to Mutagenesis Data Inproceedings In: Proceedings of the First British-Cuban Workshop on BioInformatics, 2002. @inproceedings{colton2002automatedb, title = {Automated Theory Formation Applied to Mutagenesis Data}, author = { Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_bcwob02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Proceedings of the First British-Cuban Workshop on BioInformatics}, abstract = {A theory learned by an inductive logic programming (ILP) system such as Progol [5] usually comprises a set of concepts, expressed as logic programs, which can be employed for a classification task. This classifying ability can, in turn, be used for prediction tasks. A scientific theory, however, comprises much more information: concepts; hypotheses relating concepts; explanations and empirical justifications of the hypotheses; representation schemes; experimental methodologies and so on. Working mainly in mathematics, we have used the HR system [1] to form theories about some objects of interest in a domain. For example, in group theory, where the objects are groups, HR invents concepts, makes conjectures about those concepts, and proves (some of) the conjectures using the Otter theorem prover [4]. Despite it’s history in mathematics, we have developed HR as a domain-independent machine learning program. In particular, the format for background information is very similar to that for Progol. Given this, we are currently exploring various possibilities for automated theory formation (ATF) using bioinformatics datasets. We describe here an application of HR to the mutagenesis data set [6] and suggest some advantages of ATF over ILP, some disadvantages, and some possibilities for the fruitful combination of the two techniques.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } A theory learned by an inductive logic programming (ILP) system such as Progol [5] usually comprises a set of concepts, expressed as logic programs, which can be employed for a classification task. This classifying ability can, in turn, be used for prediction tasks. A scientific theory, however, comprises much more information: concepts; hypotheses relating concepts; explanations and empirical justifications of the hypotheses; representation schemes; experimental methodologies and so on. Working mainly in mathematics, we have used the HR system [1] to form theories about some objects of interest in a domain. For example, in group theory, where the objects are groups, HR invents concepts, makes conjectures about those concepts, and proves (some of) the conjectures using the Otter theorem prover [4]. Despite it’s history in mathematics, we have developed HR as a domain-independent machine learning program. In particular, the format for background information is very similar to that for Progol. Given this, we are currently exploring various possibilities for automated theory formation (ATF) using bioinformatics datasets. We describe here an application of HR to the mutagenesis data set [6] and suggest some advantages of ATF over ILP, some disadvantages, and some possibilities for the fruitful combination of the two techniques. |

#### 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. @inproceedings{ramezani2010automatic, title = {Automatic Generation of Dynamic Investigation Problems}, author = { Ramin Ramezani and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/ramezani_arw10.pdf}, year = {2010}, date = {2010-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, pages = {34}, organization = {Citeseer}, abstract = {One of the ultimate goals of AI computer programs is to solve real world problems as efficiently, or even better than people; sometimes to even solve problems that cannot be solved by people. Imagine a crime case with many suspects involved where each of the suspects has various motivations for the murder which makes the case fairly complicated and the amount of information would be large for a detective to process. Considering that the knowledge about the crime may not even be sufficient for the detective to deduce the murderer, he/she may refer to previously solved cases which bear resemblance to the current one, hoping to find information that can be generalized to the present problem. Employing this new information may lead to identifying the murderer or to at least making it easier by excluding some of the suspects. We call such problems investigation problems, (IPs). These may exhibit ambiguity and complexity but AI problem solving techniques such as machine learning, constraint solving and automated theorem proving are considered as powerful tools for solving such problems. Having focused on investigation problems inspired us to initially come up with a formalized way of defining IPs where we present here. Furthermore, we will discuss an experiment in which different scenarios of a certain IP is generated and is solved by a Constraint Satisfaction Problem (CSP) solving approach.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } One of the ultimate goals of AI computer programs is to solve real world problems as efficiently, or even better than people; sometimes to even solve problems that cannot be solved by people. Imagine a crime case with many suspects involved where each of the suspects has various motivations for the murder which makes the case fairly complicated and the amount of information would be large for a detective to process. Considering that the knowledge about the crime may not even be sufficient for the detective to deduce the murderer, he/she may refer to previously solved cases which bear resemblance to the current one, hoping to find information that can be generalized to the present problem. Employing this new information may lead to identifying the murderer or to at least making it easier by excluding some of the suspects. We call such problems investigation problems, (IPs). These may exhibit ambiguity and complexity but AI problem solving techniques such as machine learning, constraint solving and automated theorem proving are considered as powerful tools for solving such problems. Having focused on investigation problems inspired us to initially come up with a formalized way of defining IPs where we present here. Furthermore, we will discuss an experiment in which different scenarios of a certain IP is generated and is solved by a Constraint Satisfaction Problem (CSP) solving approach. |

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. @inbook{pease2010applying, title = {Applying Lakatos-style reasoning to AI problems}, author = {Alison Pease and Alan Smaill and Simon Colton and Andrew Ireland and Maria Teresa Llano and Ramin Ramezani and Gudmund Grov and Markus Guhe}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_tm10-1.pdf}, doi = {10.4018/978-1-61692-014-2.ch010}, isbn = {9781616920142}, year = {2010}, date = {2010-01-01}, booktitle = {Thinking Machines and the philosophy of computer science: Concepts and principles.}, journal = {Thinking Machines and the philosophy of computer science: Concepts and principles}, pages = {149--174}, publisher = {Information Science Reference}, chapter = {10}, abstract = {One current direction in AI research is to focus on combining different reasoning styles such as deduction, induction, abduction, analogical reasoning, non-monotonic reasoning, vague and uncertain reasoning. The philosopher Imre Lakatos produced one such theory of how people with different reasoning styles collaborate to develop mathematical ideas. Lakatos argued that mathematics is a quasi-empirical, flexible, fallible, human endeavour, involving negotiations, mistakes, vague concept definitions and disagreements, and he outlined a heuristic approach towards the subject. In this chapter we apply these heuristics to the AI domains of evolving requirement specifi- cations, planning and constraint satisfaction problems. In drawing analogies between Lakatos’s theory and these three domains we identify areas of work which correspond to each heuristic, and suggest extensions and further ways in which Lakatos’s philoso- phy can inform AI problem solving. Thus, we show how we might begin to produce a philosophically-inspired AI theory of combined reasoning.}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } One current direction in AI research is to focus on combining different reasoning styles such as deduction, induction, abduction, analogical reasoning, non-monotonic reasoning, vague and uncertain reasoning. The philosopher Imre Lakatos produced one such theory of how people with different reasoning styles collaborate to develop mathematical ideas. Lakatos argued that mathematics is a quasi-empirical, flexible, fallible, human endeavour, involving negotiations, mistakes, vague concept definitions and disagreements, and he outlined a heuristic approach towards the subject. In this chapter we apply these heuristics to the AI domains of evolving requirement specifi- cations, planning and constraint satisfaction problems. In drawing analogies between Lakatos’s theory and these three domains we identify areas of work which correspond to each heuristic, and suggest extensions and further ways in which Lakatos’s philoso- phy can inform AI problem solving. Thus, we show how we might begin to produce a philosophically-inspired AI theory of combined reasoning. |

Ramezani, Ramin; Colton, Simon Solving Mutilated Problems Inproceedings In: Automated Reasoning Workshop, pp. 27, 2009. @inproceedings{ramezani2009solving, title = {Solving Mutilated Problems}, author = { Ramin Ramezani and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/ramezani_arw09.pdf}, year = {2009}, date = {2009-01-01}, booktitle = {Automated Reasoning Workshop}, pages = {27}, abstract = {Constraint solving, theorem proving and machine learning provide powerful techniques for solving AI problems. In all these approaches, information known as background knowledge needs to be provided, from which the system will infer new knowledge. Often, however, the background information may be obscure or incomplete, and is usually presented in a form suitable for only one type of problem solver, such as a first order theorem prover. In real world scenarios, there may not be enough background information for any single solver to solve the problem, and we are interested in cases where it may be possible to combine a machine learner, theorem prover and constraint solver in order to best use their incomplete background knowledge to solve the problem. We present here some preliminary experiments designed to test the feasibility of such an approach}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Constraint solving, theorem proving and machine learning provide powerful techniques for solving AI problems. In all these approaches, information known as background knowledge needs to be provided, from which the system will infer new knowledge. Often, however, the background information may be obscure or incomplete, and is usually presented in a form suitable for only one type of problem solver, such as a first order theorem prover. In real world scenarios, there may not be enough background information for any single solver to solve the problem, and we are interested in cases where it may be possible to combine a machine learner, theorem prover and constraint solver in order to best use their incomplete background knowledge to solve the problem. We present here some preliminary experiments designed to test the feasibility of such an approach |

Charnley, John; Colton, Simon Prediction using Machine Learned Constraint Satisfaction Programs Inproceedings In: Proceedings of the Automated Reasoning Workshop, 2007. @inproceedings{charnleyprediction, title = {Prediction using Machine Learned Constraint Satisfaction Programs}, author = { John Charnley and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/charnley_arw07.pdf}, year = {2007}, date = {2007-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, journal = {Automated Reasoning Workshop}, abstract = {Prediction is a well-researched area for Machine Learning applications. In these tasks, the aim is to predict the value for some unseen characteristic based upon the values of other, seen, characteristics for a given example. Machine learning has been extensively applied to these types of tasks by automating the derivation of a predictive function or a set of predictive rules. This predictive function can then be applied to new examples to estimate attribute values.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Prediction is a well-researched area for Machine Learning applications. In these tasks, the aim is to predict the value for some unseen characteristic based upon the values of other, seen, characteristics for a given example. Machine learning has been extensively applied to these types of tasks by automating the derivation of a predictive function or a set of predictive rules. This predictive function can then be applied to new examples to estimate attribute values. |

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. @inproceedings{charnley2006expressing, title = {Expressing General Problems as CSPs}, author = { John Charnley and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/charnley_ecai06workshop.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of the Workshop on Modelling and Solving Problems with Constraints at ECAI}, organization = {Citeseer}, abstract = {We consider the translation of general AI problems into CSPs. In particular, we have developed a translation suite able to translate first order specifica- tions into the syntax of the Sicstus CLPFD constraint solver. We describe recent extensions to the capabilities of this suite which have enabled it to handle prob- lems outside of the algebraic domains for which it was designed. We demonstrate two of many advantages to having such a translation suite. Firstly, we show that an ability to translate between the syntaxes of different AI problem solving sys- tems enables us to make meaningful comparisons of different AI techniques, and we demonstrate this using a model generator and a constraint solver on quasi- group problems. Secondly, with an ability to express a problem in different ways, we can begin to simulate more sophisticated problem solving which uses induc- tive, deductive and constraint solving techniques. We explore such possibilities with some applications to investigative reasoning, where the aim is to identify the cause of a phenomenon from a set of candidates.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We consider the translation of general AI problems into CSPs. In particular, we have developed a translation suite able to translate first order specifica- tions into the syntax of the Sicstus CLPFD constraint solver. We describe recent extensions to the capabilities of this suite which have enabled it to handle prob- lems outside of the algebraic domains for which it was designed. We demonstrate two of many advantages to having such a translation suite. Firstly, we show that an ability to translate between the syntaxes of different AI problem solving sys- tems enables us to make meaningful comparisons of different AI techniques, and we demonstrate this using a model generator and a constraint solver on quasi- group problems. Secondly, with an ability to express a problem in different ways, we can begin to simulate more sophisticated problem solving which uses induc- tive, deductive and constraint solving techniques. We explore such possibilities with some applications to investigative reasoning, where the aim is to identify the cause of a phenomenon from a set of candidates. |

Charnley, John; Colton, Simon; Miguel, Ian Automated Reformulation of Constraint Satisfaction Problems Inproceedings In: Proceedings of the Automated Reasoning Workshop, pp. 8, Citeseer, 2006. @inproceedings{charnley2006automated, title = {Automated Reformulation of Constraint Satisfaction Problems}, author = { John Charnley and Simon Colton and Ian Miguel}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/charnley_arw06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop}, journal = {Specification and Verification of Reconfiguration Protocols in Grid Component Systems}, pages = {8}, publisher = {Citeseer}, abstract = {A constraint satisfaction problem (CSP) consists of a set of variables {x1,x2,...,xn}, a set of domains of values the variables can take and a set of constraints specifying which values the variables can take simultaneously. A solution to a CSP is an assignment of values to each of the variables from their domains such that no constraints are broken. They find widespread use in science and industry and can be extremely complicated, involving a large number of variables and complex constraints. CSP solvers allow users to specify CSPs in a particular syntax, and then search for solutions to the problem, normally using a configurable search approach. Correctly formulating CSPs is a skilled and time-consuming task. Moreover, once formulated, a CSP problem can take a large amount of processing time to solve. For these reasons, various methods have been devised to improve the effectiveness of CSP solving. One such method is to find additional information about the domain being studied and use this knowledge to reformulate the CSP solver to improve its effectiveness. In particular, when the domain of investigation is described by axioms in first-order logic then it may be possible to derive new theorems from those axioms. Such implied theorems are true for all instances of the domain and can therefore be added to the CSP formulation without loss of generality.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } A constraint satisfaction problem (CSP) consists of a set of variables {x1,x2,...,xn}, a set of domains of values the variables can take and a set of constraints specifying which values the variables can take simultaneously. A solution to a CSP is an assignment of values to each of the variables from their domains such that no constraints are broken. They find widespread use in science and industry and can be extremely complicated, involving a large number of variables and complex constraints. CSP solvers allow users to specify CSPs in a particular syntax, and then search for solutions to the problem, normally using a configurable search approach. Correctly formulating CSPs is a skilled and time-consuming task. Moreover, once formulated, a CSP problem can take a large amount of processing time to solve. For these reasons, various methods have been devised to improve the effectiveness of CSP solving. One such method is to find additional information about the domain being studied and use this knowledge to reformulate the CSP solver to improve its effectiveness. In particular, when the domain of investigation is described by axioms in first-order logic then it may be possible to derive new theorems from those axioms. Such implied theorems are true for all instances of the domain and can therefore be added to the CSP formulation without loss of generality. |

Charnley, John; Colton, Simon; Miguel, Ian Automatic generation of Implied Constraints Inproceedings In: ECAI, pp. 73–77, 2006. @inproceedings{charnley2006automatic, title = {Automatic generation of Implied Constraints}, author = { John Charnley and Simon Colton and Ian Miguel}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/charnley_ecai06.pdf}, year = {2006}, date = {2006-01-01}, booktitle = {ECAI}, volume = {141}, pages = {73--77}, abstract = {A well-known difficulty with solving Constraint Satis- faction Problems (CSPs) is that, while one formulation of a CSP may enable a solver to solve it quickly, a different formulation may take prohibitively long to solve. We demonstrate a system for automati- cally reformulating CSP solver models by combining the capabilities of machine learning and automated theorem proving with CSP sys- tems. Our system is given a basic CSP formulation and outputs a set of reformulations, each of which includes additional constraints. The additional constraints are generated through a machine learn- ing process and are proven to follow from the basic formulation by a theorem prover. Experimenting with benchmark problem classes from finite algebras, we show how the time invested in reformulation is often recovered many times over when searching for solutions to more difficult problems from the problem class.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } A well-known difficulty with solving Constraint Satis- faction Problems (CSPs) is that, while one formulation of a CSP may enable a solver to solve it quickly, a different formulation may take prohibitively long to solve. We demonstrate a system for automati- cally reformulating CSP solver models by combining the capabilities of machine learning and automated theorem proving with CSP sys- tems. Our system is given a basic CSP formulation and outputs a set of reformulations, each of which includes additional constraints. The additional constraints are generated through a machine learn- ing process and are proven to follow from the basic formulation by a theorem prover. Experimenting with benchmark problem classes from finite algebras, we show how the time invested in reformulation is often recovered many times over when searching for solutions to more difficult problems from the problem class. |

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. @article{colton2005tm, title = {The TM System for Repairing Non-Theorems}, author = { Simon Colton and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ijcar04workshop.pdf}, year = {2005}, date = {2005-01-01}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {125}, number = {3}, pages = {87--101}, publisher = {Elsevier}, abstract = {We describe a flexible approach to automated reasoning, where non-theorems can be automatically altered to produce proved results which are related to the origi-nal. This is achieved in the TM system through an interaction of the HR machine learning program, the Otter theorem prover and the Mace model generator. Given a non-theorem, Mace is used to generate examples which support the non-theorem, and examples which falsify it. HR then invents concepts which categorise these examples and TM uses these concepts to modify the original non-theorem into spe-cialised theorems which Otter can prove. The methods employed by TM are inspired by the piecemeal exclusion, strategic withdrawal and counterexample barring meth-ods described in Lakatos's philosophy of mathematics. In addition, TM can also determine which modified theorems are likely to be interesting and which are not. We demonstrate the effectiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems. We show that, for 98 non-theorems, TM produced meaningful modifications for 81 of them. This work forms part of two larger projects. Firstly, we are working towards a full implementation both of the reasoning and the social interaction notions described by Lakatos. Secondly, we are aiming to show that the combination of reasoning systems such as those used in TM will lead to a new generation of more powerful AI systems. Key words: Automated theorem modification, automated reasoning, model generation, machine learning, automated theory formation, philosophy of mathematics. }, keywords = {}, pubstate = {published}, tppubtype = {article} } We describe a flexible approach to automated reasoning, where non-theorems can be automatically altered to produce proved results which are related to the origi-nal. This is achieved in the TM system through an interaction of the HR machine learning program, the Otter theorem prover and the Mace model generator. Given a non-theorem, Mace is used to generate examples which support the non-theorem, and examples which falsify it. HR then invents concepts which categorise these examples and TM uses these concepts to modify the original non-theorem into spe-cialised theorems which Otter can prove. The methods employed by TM are inspired by the piecemeal exclusion, strategic withdrawal and counterexample barring meth-ods described in Lakatos's philosophy of mathematics. In addition, TM can also determine which modified theorems are likely to be interesting and which are not. We demonstrate the effectiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems. We show that, for 98 non-theorems, TM produced meaningful modifications for 81 of them. This work forms part of two larger projects. Firstly, we are working towards a full implementation both of the reasoning and the social interaction notions described by Lakatos. Secondly, we are aiming to show that the combination of reasoning systems such as those used in TM will lead to a new generation of more powerful AI systems. Key words: Automated theorem modification, automated reasoning, model generation, machine learning, automated theory formation, philosophy of mathematics. |

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. @inproceedings{colton2005machine, title = {Machine Learning Case Splits for Theorem Proving}, author = { Simon Colton and Ferdinand Hoermann and Geoff Sutcliffe and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_arw05.pdf}, year = {2005}, date = {2005-01-01}, booktitle = {Proceedings of the Automated Reasoning Workshop, Edinburgh}, abstract = {We believe that in order to build more powerful AI systems, it will be necessary to combine techniques from machine learn-ing, automated deduction, constraint solving, computer al-gebra, planning and other domains. In particular, as argued by philosophers such as Lakatos [5], mathematical discovery processes rely on a plethora of reasoning techniques, includ-ing deduction, induction, abduction, symbolic manipulation, etc. To demonstrate that the whole can be more than the sum of the parts when combining systems, we have performed a number of case studies in automated mathematics. These demonstrate that, with respect to stand-alone systems, com-bined reasoning systems can: (a) be more flexible in their application [4] (b) undertake new tasks [2] and (c) perform standard tasks better [3]. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We believe that in order to build more powerful AI systems, it will be necessary to combine techniques from machine learn-ing, automated deduction, constraint solving, computer al-gebra, planning and other domains. In particular, as argued by philosophers such as Lakatos [5], mathematical discovery processes rely on a plethora of reasoning techniques, includ-ing deduction, induction, abduction, symbolic manipulation, etc. To demonstrate that the whole can be more than the sum of the parts when combining systems, we have performed a number of case studies in automated mathematics. These demonstrate that, with respect to stand-alone systems, com-bined reasoning systems can: (a) be more flexible in their application [4] (b) undertake new tasks [2] and (c) perform standard tasks better [3]. |

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. @inbook{Pease2004, title = {Automatic Conjecture Modification}, author = {Alison Pease and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/pease_arw04.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {Proceedings of the 11th Workshop On Automated Reasoning: Bridging The Gap Between Theory And Practice}, abstract = {One of the original goals of writing theorem provers was to provide tools which mathematicians could use to aid their research, yet this goal remains unsatisfied to a large extent. We believe that one of the reasons for this failure is that so far automated theorem provers have failed to incorporate the flexibility which humans take for granted, and which is inherent in intelligent activity. To begin to address this, we have implemented a theorem modification system, called TM. This is able to take in a conjecture, try to prove it, and if unsuccessful (either because the conjecture is too hard to prove or because it is false), produce modified versions of the conjecture which it can prove. As a simple, yet illustrative, example, given the non-theorem that all groups are Abelian, TM states that it cannot prove the original result, but it has discovered that all self-inverse groups are Abelian. TM is a combined reasoning system, which uses inductive, deductive and model-based reasoning to achieve the goal of modifying theorems. }, keywords = {}, pubstate = {published}, tppubtype = {inbook} } One of the original goals of writing theorem provers was to provide tools which mathematicians could use to aid their research, yet this goal remains unsatisfied to a large extent. We believe that one of the reasons for this failure is that so far automated theorem provers have failed to incorporate the flexibility which humans take for granted, and which is inherent in intelligent activity. To begin to address this, we have implemented a theorem modification system, called TM. This is able to take in a conjecture, try to prove it, and if unsuccessful (either because the conjecture is too hard to prove or because it is false), produce modified versions of the conjecture which it can prove. As a simple, yet illustrative, example, given the non-theorem that all groups are Abelian, TM states that it cannot prove the original result, but it has discovered that all self-inverse groups are Abelian. TM is a combined reasoning system, which uses inductive, deductive and model-based reasoning to achieve the goal of modifying theorems. |

Colton, Simon; Pease, Alison Lakatos-style automated theorem modification Inproceedings In: ECAI, pp. 977, 2004. @inproceedings{colton2004lakatos, title = {Lakatos-style automated theorem modification}, author = { Simon Colton and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ecai04poster.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {ECAI}, volume = {16}, pages = {977}, abstract = {We describe a flexible approach to automated reasoning, where non-theorems can be automatically altered to produce proved results which are related to the original. This is achieved through an interaction of the HR machine learning system, the Otter theorem prover and the Mace model generator, and uses methods inspired by Lakatos’s philosophy of mathematics. We demonstrate the effec- tiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We describe a flexible approach to automated reasoning, where non-theorems can be automatically altered to produce proved results which are related to the original. This is achieved through an interaction of the HR machine learning system, the Otter theorem prover and the Mace model generator, and uses methods inspired by Lakatos’s philosophy of mathematics. We demonstrate the effec- tiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems. |

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. @inproceedings{sutcliffe2003grand, title = {A Grand Challenge of Theorem Discovery}, author = { Geoff Sutcliffe and Yi Gao and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/sutcliffe_cade03.pdf}, year = {2003}, date = {2003-01-01}, booktitle = {Proceedings of the Workshop on Challenges and Novel Applications for Automated Reasoning, 19th International Conference on Automated Reasoning}, pages = {1--11}, abstract = {A primary mode of operation of ATP systems is to supply the system with axioms and a conjecture, and to then ask the system to produce a proof (or at least an assurance that there is a proof) that the conjecture is a theorem of the axioms. This paper challenges ATP to a new mode of operation, by which interesting theorems are generated from a set of axioms. The challenge requires solutions to both theoretical and computational issues. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } A primary mode of operation of ATP systems is to supply the system with axioms and a conjecture, and to then ask the system to produce a proof (or at least an assurance that there is a proof) that the conjecture is a theorem of the axioms. This paper challenges ATP to a new mode of operation, by which interesting theorems are generated from a set of axioms. The challenge requires solutions to both theoretical and computational issues. |

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. @inproceedings{Zimmer2002, title = {Integrating HR and tptp2x into MathWeb to Compare Automated Theorem Provers}, author = { Jürgen Zimmer and Andreas Franke and Simon Colton and Geoff Sutcliffe}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/zimmer_paps02.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {In Proceedings of the CADE'02 Workshop on Problems and Problem sets}, organization = {Citeseer}, abstract = {The assessment and comparison of automated theorem proving sys-tems (ATPs) is important for the advancement of the field. At present, the de facto assessment method is to test provers on the TPTP library of nearly 6000 theorems. We describe here a project which aims to com-plement the TPTP service by automatically generating theorems of suf-ficient difficulty to provide a significant test for first order provers. This has been achieved by integrating the HR automated theory formation program into the MathWeb Software Bus. HR generates first order con-jectures in TPTP format and passes them to a concurrent ATP service in MathWeb. MathWeb then uses the tptp2X utility to translate the conjectures into the input format of a set of provers. In this way, var-ious ATP systems can be compared on their performance over sets of thousands of theorems they have not been previously exposed to. Our purpose here is to describe the integration of various new programs into the MathWeb architecture, rather than to present a full analysis of the performance of theorem provers. However, to demonstrate the potential of the combination of the systems, we describe some preliminary results from experiments in group theory. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The assessment and comparison of automated theorem proving sys-tems (ATPs) is important for the advancement of the field. At present, the de facto assessment method is to test provers on the TPTP library of nearly 6000 theorems. We describe here a project which aims to com-plement the TPTP service by automatically generating theorems of suf-ficient difficulty to provide a significant test for first order provers. This has been achieved by integrating the HR automated theory formation program into the MathWeb Software Bus. HR generates first order con-jectures in TPTP format and passes them to a concurrent ATP service in MathWeb. MathWeb then uses the tptp2X utility to translate the conjectures into the input format of a set of provers. In this way, var-ious ATP systems can be compared on their performance over sets of thousands of theorems they have not been previously exposed to. Our purpose here is to describe the integration of various new programs into the MathWeb architecture, rather than to present a full analysis of the performance of theorem provers. However, to demonstrate the potential of the combination of the systems, we describe some preliminary results from experiments in group theory. |

Colton, Simon; Sutcliffe, Geoff Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems. Inproceedings In: AMAI, 2002. @inproceedings{Colton2002, title = {Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems.}, author = { Simon Colton and Geoff Sutcliffe}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_aim02_2.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {AMAI}, abstract = {Automated Theorem Proving (ATP) researchers who always use the same problems for testing their systems, run the risk of producing systems that can solve only those problems, and are weak on new problems or applications. Furthermore, as the state-of-the-art in ATP progresses, existing test problems become too easy, and testing on them provides little useful information. It is thus important to regularly find new and harder problems for testing ATP systems. HR is a program that performs automated theory formation in mathematical domains, such as group theory, quasigroup theory, and ring theory. Given the axioms of the domain, HR invents concepts, finds examples of them using a model generator, and makes conjectures empirically about the concepts. HR has been used to discover new group theory theorems of sufficient difficulty to be included in the TPTP - the standard library of test problems for first order ATP systems. As HR produces tens of thousands of distinct theorems, there has also been an opportunity to determine some characteristics that can be used to identify hard problems. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Automated Theorem Proving (ATP) researchers who always use the same problems for testing their systems, run the risk of producing systems that can solve only those problems, and are weak on new problems or applications. Furthermore, as the state-of-the-art in ATP progresses, existing test problems become too easy, and testing on them provides little useful information. It is thus important to regularly find new and harder problems for testing ATP systems. HR is a program that performs automated theory formation in mathematical domains, such as group theory, quasigroup theory, and ring theory. Given the axioms of the domain, HR invents concepts, finds examples of them using a model generator, and makes conjectures empirically about the concepts. HR has been used to discover new group theory theorems of sufficient difficulty to be included in the TPTP - the standard library of test problems for first order ATP systems. As HR produces tens of thousands of distinct theorems, there has also been an opportunity to determine some characteristics that can be used to identify hard problems. |

Colton, Simon Automated Theorem Discovery: Future Direction for Theorem Provers Miscellaneous 2001. @misc{Colton2001, title = {Automated Theorem Discovery: Future Direction for Theorem Provers}, author = {Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_ijcar01.pdf}, year = {2001}, date = {2001-01-01}, abstract = {One obvious and important aspect of automated theorem proving is that the users know in advance which theorem they wish to prove. A possible future direction for theorem provers is to enable users to discover theorems which they were not necessarily aware of. We sur-vey previous attempts at this and give a new demonstration of theorem generation using our HR program [10] in the domain of 'anti-associative' algebras. We also suggest three applications where this functionality may prove useful, and discuss how this would add value to theorem provers. }, keywords = {}, pubstate = {published}, tppubtype = {misc} } One obvious and important aspect of automated theorem proving is that the users know in advance which theorem they wish to prove. A possible future direction for theorem provers is to enable users to discover theorems which they were not necessarily aware of. We sur-vey previous attempts at this and give a new demonstration of theorem generation using our HR program [10] in the domain of 'anti-associative' algebras. We also suggest three applications where this functionality may prove useful, and discuss how this would add value to theorem provers. |

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. @inproceedings{Colton2001, title = {Constraint Generation via Automated Theory Formation}, author = { Simon Colton and Ian Miguel}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/colton_cp01.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {International Conference on Principles and Practice of Constraint Programming}, pages = {575--579}, organization = {Springer}, abstract = {Adding constraints to a basic CSP model can significantly reduce search, e.g. for Golomb rulers [6]. The generation process is usually performed by hand, although some recent work has focused on automatically generating symmetry breaking constraints [4] and (less so) on generating implied constraints [5]. We describe an approach to generating implied, symmetry breaking and specialisa-tion constraints and apply this technique to quasigroup construction [10]. Given a problem class parameterised by size, we use a basic model to solve small instances with the Choco constraint programming language [7]. We then give these solutions to the HR automated theory formation program [1] which detects implied constraints (proved to follow from the specifications) and in-duced constraints (true of a subset of solutions). Interpreting HR's results to reformulate the model can lead to a reduction in search on larger instances. It is often more efficient to run HR, interpret the results and solve the CSP, than to solve the problem with the basic model alone. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Adding constraints to a basic CSP model can significantly reduce search, e.g. for Golomb rulers [6]. The generation process is usually performed by hand, although some recent work has focused on automatically generating symmetry breaking constraints [4] and (less so) on generating implied constraints [5]. We describe an approach to generating implied, symmetry breaking and specialisa-tion constraints and apply this technique to quasigroup construction [10]. Given a problem class parameterised by size, we use a basic model to solve small instances with the Choco constraint programming language [7]. We then give these solutions to the HR automated theory formation program [1] which detects implied constraints (proved to follow from the specifications) and in-duced constraints (true of a subset of solutions). Interpreting HR's results to reformulate the model can lead to a reduction in search on larger instances. It is often more efficient to run HR, interpret the results and solve the CSP, than to solve the problem with the basic model alone. |

Colton, Simon Theory Formation Applied to Learning, Discovery and Problem Solving Inproceedings In: Proceedings of Machine Intelligence 17, 2000. @inproceedings{Colton2000, title = {Theory Formation Applied to Learning, Discovery and Problem Solving}, author = {Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/colton_mi00.pdf}, year = {2000}, date = {2000-01-01}, booktitle = {Proceedings of Machine Intelligence 17}, abstract = {We discuss the HR program [1] which is designed to perform automated theory formation in domains of pure mathematics. We overview the recent application of theory formation to discovery, learning and problem solving tasks. We compare how theory formation is used for these tasks and discuss how to compare HR to the machine learning program Progol [9]. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We discuss the HR program [1] which is designed to perform automated theory formation in domains of pure mathematics. We overview the recent application of theory formation to discovery, learning and problem solving tasks. We compare how theory formation is used for these tasks and discuss how to compare HR to the machine learning program Progol [9]. |