Alison Pease
Lecturer (Dundee)
About me
I recently moved to the School of Computing at the University Dundee, to take up a lectureship in the Argumentation and Computation research group. Previously, I was a Research Associate working in the Computational Creativity Group at Imperial College London (now at Goldsmiths), and the Theory Group at Queen Mary, University of London. I am also a visiting researcher at the University of Edinburgh, and I currently have my main web pages here.
The Computational Creativity Theory Project
I am working with Simon Colton and John Charnley to develop a rigorous, computationally detailed and plausible account of how creation by software could occur. We use examples and theories of human creativity, particularly in the visual arts and in mathematics, to inspire our development of formalisms to describe and extend the notion of creativity in software.
Researching Mathematical Practice
I am working with Ursula Martin to investigate current mathematical practice; in particular, ways in which mathematicians are using web 2.0 technology. We are interested in whether Lakatos’s theory of how mathematicians communicate and use counterexamples to refine concepts, conjectures and proofs was an accurate description of evolution in mathematics, and whether Polya’s problem solving heuristics are used in research mathematics.
You can contact me on .[at]...
Publications
Corneli, Joe; Guckelsberger, Christian; Jordanous, Anna; Pease, Alison; Colton, Simon; Erden, Yasemin J Conference Report: AISB Members Workshop VII – Serendipity Symposium Miscellaneous AISB Quarterly (147), 2017. @misc{Corneli2017AISBQ, title = {Conference Report: AISB Members Workshop VII – Serendipity Symposium}, author = {Joe Corneli and Christian Guckelsberger and Anna Jordanous and Alison Pease and Simon Colton and Yasemin J. Erden}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2017/09/serendipity_symposium_report_AISBQ.pdf}, year = {2017}, date = {2017-08-01}, howpublished = {AISB Quarterly (147)}, keywords = {}, pubstate = {published}, tppubtype = {misc} } |
Colton, Simon; Pease, Alison; Corneli, Joseph; Cook, Michael; Hepworth, Rose; Ventura, Dan Stakeholder Groups in Computational Creativity Research and Practice Incollection In: Computational Creativity Research: Towards Creative Machines, pp. 3–36, Springer, 2015. @incollection{colton2015stakeholder, title = {Stakeholder Groups in Computational Creativity Research and Practice}, author = { Simon Colton and Alison Pease and Joseph Corneli and Michael Cook and Rose Hepworth and Dan Ventura}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/colton_ccchapter15.pdf}, year = {2015}, date = {2015-01-01}, booktitle = {Computational Creativity Research: Towards Creative Machines}, pages = {3--36}, publisher = {Springer}, abstract = {The notion that software could be independently and usefully creative is becoming more commonplace in scientific, cultural, business and public circles. It is not fanciful to imagine creative software embedded in society in the short to medium term, acting as collaborators and autonomous creative agents for much societal benefit. Technologically, there is still some way to go to enable Artificial Intelligence methods to create artefacts and ideas of value, and to get software to do so in interesting and engaging ways. There are also a number of sociological hurdles to overcome in getting society to accept software as being truly creative, and we concentrate on those here. We discuss the various communities that can be considered stakeholders in the perception of computers being creative or not. In particular, we look in detail at three sets of stakeholders, namely the general public, Computational Creativity researchers and fellow creatives.We put forward various philosophical points which we argue will shape the way in which society accepts creative software. We make various claims along the way about how people perceive software as being creative or not, which we believe should be addressed with scientific experimentation, and we call on the Computational Creativity research community to do just that.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} } The notion that software could be independently and usefully creative is becoming more commonplace in scientific, cultural, business and public circles. It is not fanciful to imagine creative software embedded in society in the short to medium term, acting as collaborators and autonomous creative agents for much societal benefit. Technologically, there is still some way to go to enable Artificial Intelligence methods to create artefacts and ideas of value, and to get software to do so in interesting and engaging ways. There are also a number of sociological hurdles to overcome in getting society to accept software as being truly creative, and we concentrate on those here. We discuss the various communities that can be considered stakeholders in the perception of computers being creative or not. In particular, we look in detail at three sets of stakeholders, namely the general public, Computational Creativity researchers and fellow creatives.We put forward various philosophical points which we argue will shape the way in which society accepts creative software. We make various claims along the way about how people perceive software as being creative or not, which we believe should be addressed with scientific experimentation, and we call on the Computational Creativity research community to do just that. |
Colton, Simon; Cook, Michael; Hepworth, Rose; Pease, Alison On Acid Drops and Teardrops: Observer Issues in Computational Creativity Inproceedings In: Proceedings of the 7th AISB Symposium on Computing and Philosophy, 2014. @inproceedings{colton2014acid, title = {On Acid Drops and Teardrops: Observer Issues in Computational Creativity}, author = { Simon Colton and Michael Cook and Rose Hepworth and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/colton_aisb14c.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the 7th AISB Symposium on Computing and Philosophy}, abstract = {We argue that the notion of creativity in a person or software is a secondary and essentially contested concept. Hence, in Computational Creativity research – where we aim to build software taken seriously as independently creative – understanding the roles people take as process observer and product consumer is paramount. Depending on the domain, there can be a natural bias against software created artefacts, and Computational Creativity researchers have exacerbated this situation through Turing-style comparison tests. Framing this as a modified Chinese Room experiment, we propose two remedies to the situation. These involve software accounting for its decisions, actions and products, and taking the radical step of thinking of computer generated artefacts as fundamentally different to their human-produced counterparts. We use two case studies, where people interact with an automated painter and with computer-generated videogames, to highlight the observer issues we raise, and to demonstrate partial implementations of our remedies.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We argue that the notion of creativity in a person or software is a secondary and essentially contested concept. Hence, in Computational Creativity research – where we aim to build software taken seriously as independently creative – understanding the roles people take as process observer and product consumer is paramount. Depending on the domain, there can be a natural bias against software created artefacts, and Computational Creativity researchers have exacerbated this situation through Turing-style comparison tests. Framing this as a modified Chinese Room experiment, we propose two remedies to the situation. These involve software accounting for its decisions, actions and products, and taking the radical step of thinking of computer generated artefacts as fundamentally different to their human-produced counterparts. We use two case studies, where people interact with an automated painter and with computer-generated videogames, to highlight the observer issues we raise, and to demonstrate partial implementations of our remedies. |
Colton, Simon; Pease, Alison; Corneli, Joseph; Cook, Michael; Llano, Maria Teresa Assessing Progress in Building Autonomously Creative Systems Inproceedings In: Proceedings of the Fifth International Conference on Computational Creativity, pp. 137–145, 2014. @inproceedings{colton2014assessing, title = {Assessing Progress in Building Autonomously Creative Systems}, author = { Simon Colton and Alison Pease and Joseph Corneli and Michael Cook and Maria Teresa Llano}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/colton_iccc2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the Fifth International Conference on Computational Creativity}, pages = {137--145}, abstract = {Determining conclusively whether a new version of software creatively exceeds a previous version or a third party system is dicult, yet very important for scientific approaches in Computational Creativity research. We argue that software product and process need to be assessed simultaneously in assessing progress, and we introduce a diagrammatic formalism which exposes various timelines of creative acts in the construction and execution of successive versions of artefactgenerating software. The formalism enables estimations of progress or regress from system to system by comparing their diagrams and assessing changes in quality, quantity and variety of creative acts undertaken; audience perception of behaviours; and the quality of artefacts produced. We present a case study in the building of evolutionary art systems, and we use the formalism to highlight various issues in measuring progress in the building of creative systems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Determining conclusively whether a new version of software creatively exceeds a previous version or a third party system is dicult, yet very important for scientific approaches in Computational Creativity research. We argue that software product and process need to be assessed simultaneously in assessing progress, and we introduce a diagrammatic formalism which exposes various timelines of creative acts in the construction and execution of successive versions of artefactgenerating software. The formalism enables estimations of progress or regress from system to system by comparing their diagrams and assessing changes in quality, quantity and variety of creative acts undertaken; audience perception of behaviours; and the quality of artefacts produced. We present a case study in the building of evolutionary art systems, and we use the formalism to highlight various issues in measuring progress in the building of creative systems. |
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. |
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. |
Pease, Alison; Colton, Simon; Ramezani, Ramin; Charnley, John; Reed, Kate A Discussion on Serendipity in Creative Systems Inproceedings In: Proceedings of the Fourth International Conference on Computational Creativity, pp. 64–71, 2013. @inproceedings{pease2013discussion, title = {A Discussion on Serendipity in Creative Systems}, author = { Alison Pease and Simon Colton and Ramin Ramezani and John Charnley and Kate Reed}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_iccc13.pdf}, year = {2013}, date = {2013-01-01}, booktitle = {Proceedings of the Fourth International Conference on Computational Creativity}, pages = {64--71}, abstract = {We investigate serendipity, or happy, accidental discoveries, in CC, and propose computational concepts related to serendipity. These include a focus-shift, a breakdown of serendipitous discovery into prepared mind, serendipity trigger, bridge and result and three dimensions of serendipity: chance, sagacity and value. We propose a definition and standards for computational serendipity and evaluate three creative systems with respect to our standards. We argue that this is an important notion in creativity and, if carefully developed and used with caution, could result in a valuable new discovery technique in CC.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We investigate serendipity, or happy, accidental discoveries, in CC, and propose computational concepts related to serendipity. These include a focus-shift, a breakdown of serendipitous discovery into prepared mind, serendipity trigger, bridge and result and three dimensions of serendipity: chance, sagacity and value. We propose a definition and standards for computational serendipity and evaluate three creative systems with respect to our standards. We argue that this is an important notion in creativity and, if carefully developed and used with caution, could result in a valuable new discovery technique in CC. |
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. |
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. |
Cook, Michael; Colton, Simon; Pease, Alison Aesthetic Considerations for Automated Platformer Design Inproceedings In: Proceedings of the 8th AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment, 2012. @inproceedings{Cook2012AIIDE, title = {Aesthetic Considerations for Automated Platformer Design}, author = {Michael Cook and Simon Colton and Alison Pease}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/11/cook_aiide12.pdf}, year = {2012}, date = {2012-11-01}, booktitle = {Proceedings of the 8th AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment}, abstract = {We describe ANGELINA3, a system that can automati- cally develop games along a defined theme, by select- ing appropriate multimedia content from a variety of sources and incorporating it into a game’s design. We discuss these capabilities in the context of the FACE model for assessing progress in the building of cre- ative systems, and discuss how ANGELINA3 can be improved through further work.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We describe ANGELINA3, a system that can automati- cally develop games along a defined theme, by select- ing appropriate multimedia content from a variety of sources and incorporating it into a game’s design. We discuss these capabilities in the context of the FACE model for assessing progress in the building of cre- ative systems, and discuss how ANGELINA3 can be improved through further work. |
Pease, Alison; Colton, Simon; Charnley, John The Turing Test and Computational Creativity Inproceedings In: Contributed talks proceedings of the Turing Centenary Conference, 2012. @inproceedings{Pease2012Turing, title = {The Turing Test and Computational Creativity}, author = {Alison Pease and Simon Colton and John Charnley}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/11/pease_tc12.pdf}, year = {2012}, date = {2012-11-01}, booktitle = {Contributed talks proceedings of the Turing Centenary Conference}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
Charnley, John; Pease, Alison; Colton, Simon On the Notion of Framing in Computational Creativity Inproceedings In: Proceedings of the Third International Conference on Computational Creativity, pp. 77–81, 2012. @inproceedings{charnley2012notion, title = {On the Notion of Framing in Computational Creativity}, author = { John Charnley and Alison Pease and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/charnley_iccc12.pdf}, year = {2012}, date = {2012-01-01}, booktitle = {Proceedings of the Third International Conference on Computational Creativity}, pages = {77--81}, abstract = {In most domains, artefacts and the creativity that went into their production is judged within a context; where a context may include background information on how the creator feels about their work, what they think it expresses, how it fits in with other work done within their community, their mood before, during and after creation, and so on. We identify areas of framing information, such as motivation, intention, or the processes involved in creating a work, and consider how these areas might be applicable to the context of Computational Creativity. We suggest examples of how such framing information may be derived in existing creative systems and propose a novel dually-creative approach to framing, whereby an automated story generation system is employed, in tandem with the artefact generator, to produce suitable framing information. We outline how this method might be developed and some longer term goals.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In most domains, artefacts and the creativity that went into their production is judged within a context; where a context may include background information on how the creator feels about their work, what they think it expresses, how it fits in with other work done within their community, their mood before, during and after creation, and so on. We identify areas of framing information, such as motivation, intention, or the processes involved in creating a work, and consider how these areas might be applicable to the context of Computational Creativity. We suggest examples of how such framing information may be derived in existing creative systems and propose a novel dually-creative approach to framing, whereby an automated story generation system is employed, in tandem with the artefact generator, to produce suitable framing information. We outline how this method might be developed and some longer term goals. |
Pease, Alison; Charnley, John; Colton, Simon Using Grounded Theory to Suggest Types of Framing Information for Computational Creativity Book Chapter In: Proceedings of the Workshop "Computational Creativity, Concept Invention, and General Intelligence", pp. 7–13, University of Osnabrück, Institute of Cognitive Science, 2012. @inbook{pease2012using, title = {Using Grounded Theory to Suggest Types of Framing Information for Computational Creativity}, author = { Alison Pease and John Charnley and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_c3g12.pdf}, year = {2012}, date = {2012-01-01}, booktitle = {Proceedings of the Workshop "Computational Creativity, Concept Invention, and General Intelligence"}, pages = {7--13}, publisher = {University of Osnabrück, Institute of Cognitive Science}, series = {PICS Publications of the Institute of Cognitive Science}, abstract = {In most domains, artefacts and the creativity that went into their production is judged within a context; where a context may include background information on how the creator feels about their work, what they think it expresses, how it fits in with other work done within their community, and so on. In some cases, such framing information may involve obfuscation in order to add mystery to the work or its creator, which can add to our perception of creativity.We describe a novel method for the analysis of human creativity, using grounded theory.We demonstrate the importance of grounded theory via an ethnographic study of interviews by John Tusa with contemporary artists. By exploring the type of context and background that the artists share, we have developed theories which highlight the importance of areas of framing information, such as motivation, intention, or the processes involved in creating a work. We extend this to consider the role of mystery and obfuscation in framing, by considering what artists do not say versus what is explicitly revealed.}, keywords = {}, pubstate = {published}, tppubtype = {inbook} } In most domains, artefacts and the creativity that went into their production is judged within a context; where a context may include background information on how the creator feels about their work, what they think it expresses, how it fits in with other work done within their community, and so on. In some cases, such framing information may involve obfuscation in order to add mystery to the work or its creator, which can add to our perception of creativity.We describe a novel method for the analysis of human creativity, using grounded theory.We demonstrate the importance of grounded theory via an ethnographic study of interviews by John Tusa with contemporary artists. By exploring the type of context and background that the artists share, we have developed theories which highlight the importance of areas of framing information, such as motivation, intention, or the processes involved in creating a work. We extend this to consider the role of mystery and obfuscation in framing, by considering what artists do not say versus what is explicitly revealed. |
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; Colton, Simon On Impact and Evaluation in Computational Creativity: A Discussion of the Turing Test and an Alternative Proposal Inproceedings In: Proceedings of the AISB symposium on AI and Philosophy, 2011. @inproceedings{pease2011impact, title = {On Impact and Evaluation in Computational Creativity: A Discussion of the Turing Test and an Alternative Proposal}, author = { Alison Pease and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_aisb11.pdf}, year = {2011}, date = {2011-01-01}, booktitle = {Proceedings of the AISB symposium on AI and Philosophy}, abstract = {Computational Creativity is the AI subfield in which we study how to build computational models of creative thought in science and the arts. From an engineering perspective, it is desirable to have concrete measures for assessing the progress made from one version of a program to another, or for comparing and contrasting different software systems for the same creative task. We describe the Turing Test and versions of it which have been used in order to measure progress in Computational Creativity. We show that the versions proposed thus far lack the important aspect of interaction, without which much of the power of the Turing Test is lost. We argue that the Turing Test is largely inappropriate for the purposes of evaluation in Computational Creativity, since it attempts to homogenize creativity into a single (human) style, does not take into account the importance of background and contextual information for a creative act, encourages superficial, uninteresting advances in front-ends, and rewards creativity which adheres to a certain style over that which creates something which is genuinely novel. We further argue that although there may be some place for Turing-style tests for Computational Creativity at some point in the future, it is currently untenable to apply any defensible version of the Turing Test. As an alternative to Turing-style tests, we introduce two descriptive models for evaluating creative software, the FACE model which describes creative acts performed by software in terms of tuples of generative acts, and the IDEA model which describes how such creative acts can have an impact upon an ideal audience, given ideal information about background knowledge and the software development process. While these models require further study and elaboration, we believe that they can be usefully applied to current systems as well as guiding further development of creative systems.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Computational Creativity is the AI subfield in which we study how to build computational models of creative thought in science and the arts. From an engineering perspective, it is desirable to have concrete measures for assessing the progress made from one version of a program to another, or for comparing and contrasting different software systems for the same creative task. We describe the Turing Test and versions of it which have been used in order to measure progress in Computational Creativity. We show that the versions proposed thus far lack the important aspect of interaction, without which much of the power of the Turing Test is lost. We argue that the Turing Test is largely inappropriate for the purposes of evaluation in Computational Creativity, since it attempts to homogenize creativity into a single (human) style, does not take into account the importance of background and contextual information for a creative act, encourages superficial, uninteresting advances in front-ends, and rewards creativity which adheres to a certain style over that which creates something which is genuinely novel. We further argue that although there may be some place for Turing-style tests for Computational Creativity at some point in the future, it is currently untenable to apply any defensible version of the Turing Test. As an alternative to Turing-style tests, we introduce two descriptive models for evaluating creative software, the FACE model which describes creative acts performed by software in terms of tuples of generative acts, and the IDEA model which describes how such creative acts can have an impact upon an ideal audience, given ideal information about background knowledge and the software development process. While these models require further study and elaboration, we believe that they can be usefully applied to current systems as well as guiding further development of creative systems. |
Pease, Alison; Colton, Simon Computational Creativity Theory: Inspirations Behind the FACE and the IDEA Models Inproceedings In: Proceedings of the Second International Conference on Computational Creativity, 2011. @inproceedings{pease2011computational, title = {Computational Creativity Theory: Inspirations Behind the FACE and the IDEA Models}, author = { Alison Pease and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_iccc11.pdf}, year = {2011}, date = {2011-01-01}, booktitle = {Proceedings of the Second International Conference on Computational Creativity}, abstract = {We introduce two descriptive models for evaluating creative software; the FACE model, which describes creative acts performed by software in terms of tuples of generative acts, and the IDEA model, which describes how such creative acts can have an impact upon an audience. We show how these models have been inspired both by ideas in the psychology of creativity and by an analysis of acts of human creativity.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We introduce two descriptive models for evaluating creative software; the FACE model, which describes creative acts performed by software in terms of tuples of generative acts, and the IDEA model, which describes how such creative acts can have an impact upon an audience. We show how these models have been inspired both by ideas in the psychology of creativity and by an analysis of acts of human creativity. |
Colton, Simon; Pease, Alison; Charnley, John Computational Creativity Theory: The FACE and IDEA Descriptive Models Inproceedings In: Proceedings of the Second International Conference on Computational Creativity, pp. 90–95, 2011. @inproceedings{colton2011computational, title = {Computational Creativity Theory: The FACE and IDEA Descriptive Models}, author = { Simon Colton and Alison Pease and John Charnley}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/colton_iccc11.pdf}, year = {2011}, date = {2011-01-01}, booktitle = {Proceedings of the Second International Conference on Computational Creativity}, pages = {90--95}, abstract = {We introduce computational creativity theory (CCT) as an analogue in computational creativity research to computational learning theory in machine learning. In its current draft, CCT comprises the FACE descriptive model of creative acts as tuples of generative acts, and the IDEA descriptive model of the impact such creative acts may have. To introduce these, we simplify various assumptions about software development, background material given to software, how creative acts are performed by computer, and how audiences consume the results. We use the two descriptive models to perform two comparisons studies, firstly for mathematical discovery software, and secondly for visual art generating programs. We conclude by discussing possible additions, improvements and refinements to CCT.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We introduce computational creativity theory (CCT) as an analogue in computational creativity research to computational learning theory in machine learning. In its current draft, CCT comprises the FACE descriptive model of creative acts as tuples of generative acts, and the IDEA descriptive model of the impact such creative acts may have. To introduce these, we simplify various assumptions about software development, background material given to software, how creative acts are performed by computer, and how audiences consume the results. We use the two descriptive models to perform two comparisons studies, firstly for mathematical discovery software, and secondly for visual art generating programs. We conclude by discussing possible additions, improvements and refinements to CCT. |
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. |
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. |
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. |
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. |
Pease, Alison; Smaill, Alan; Colton, Simon; Lee, John Bridging the Gap Between Argumentation Theory and the Philosophy of Mathematics Journal Article In: Foundations of Science, 14 (1-2), pp. 111–135, 2009. @article{pease2009bridging, title = {Bridging the Gap Between Argumentation Theory and the Philosophy of Mathematics}, author = { Alison Pease and Alan Smaill and Simon Colton and John Lee}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_fos09.pdf}, year = {2009}, date = {2009-01-01}, journal = {Foundations of Science}, volume = {14}, number = {1-2}, pages = {111--135}, publisher = {Springer}, abstract = {We argue that there are mutually beneficial connections to be made between ideas in argumentation theory and the philosophy of mathematics, and that these connections can be suggested via the process of producing computational models of theories in these domains.We discuss Lakatos’s work (1976) in which he championed the informal nature of mathematics, and our computational representation of his theory. In particular, we outline our representation of Cauchy’s proof of Euler’s conjecture, which uses work by Haggith on argumentation structures, and identify connections between these structures and Lakatos’s methods.}, keywords = {}, pubstate = {published}, tppubtype = {article} } We argue that there are mutually beneficial connections to be made between ideas in argumentation theory and the philosophy of mathematics, and that these connections can be suggested via the process of producing computational models of theories in these domains.We discuss Lakatos’s work (1976) in which he championed the informal nature of mathematics, and our computational representation of his theory. In particular, we outline our representation of Cauchy’s proof of Euler’s conjecture, which uses work by Haggith on argumentation structures, and identify connections between these structures and Lakatos’s methods. |
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; 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. |
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. |
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. |
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 Lakatos and Machine Creativity Inproceedings In: Second Workshop on Creative Systems, Approaches to Creativity in Artificial Intelligence and Cognitive Science at the European Conference on Artificial Intelligence (ECAI 2002), 2002. @inproceedings{pease2002lakatos, title = {Lakatos and Machine Creativity}, author = { Alison Pease and Simon Colton and Alan Smaill and John Lee}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_ecai02workshop.pdf}, year = {2002}, date = {2002-01-01}, booktitle = {Second Workshop on Creative Systems, Approaches to Creativity in Artificial Intelligence and Cognitive Science at the European Conference on Artificial Intelligence (ECAI 2002)}, abstract = {We argue that Lakatos’ work on the history and philosophy of mathematics is of key relevance to machine creativity as it suggests ways in which to explore and transform concept spaces, rerepresent knowledge and change evaluation criteria. We describe approaches to implementing methods which Lakatos identifies, including our own approach, which extends Colton’s HR and has enabled us to automatically generate mathematical conjectures, concepts and examples which were previously impossible in HR - including Goldbach’s conjecture. The methods are of general importance as they can be applied to many domains - we describe their theoretical application to game plans, two-dimensional geometry, moral philosophy, philosophy of mind, political argument and meta-level reasoning.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We argue that Lakatos’ work on the history and philosophy of mathematics is of key relevance to machine creativity as it suggests ways in which to explore and transform concept spaces, rerepresent knowledge and change evaluation criteria. We describe approaches to implementing methods which Lakatos identifies, including our own approach, which extends Colton’s HR and has enabled us to automatically generate mathematical conjectures, concepts and examples which were previously impossible in HR - including Goldbach’s conjecture. The methods are of general importance as they can be applied to many domains - we describe their theoretical application to game plans, two-dimensional geometry, moral philosophy, philosophy of mind, political argument and meta-level reasoning. |
Colton, Simon; Pease, Alison; Ritchie, Graeme The Effect of Input Knowledge on Creativity Inproceedings In: Proceedings of the ICCBR'01 Workshop on Creative Systems, 2001. @inproceedings{colton2001effect, title = {The Effect of Input Knowledge on Creativity}, author = { Simon Colton and Alison Pease and Graeme Ritchie}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/colton_iccbr01.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {Proceedings of the ICCBR'01 Workshop on Creative Systems}, abstract = {Recently, many programs have been written to perform tasks which are usually regarded as requiring creativity in humans. We can derive some commonalities between these programs in order to build further creative programs. Key to this is the derivation of certain measures which assess how creative a program is. Starting from recent proposals by Ritchie, we define possible measures which describe the extent to which a program produces novel output. We discuss how this relates to the creativity of the program.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Recently, many programs have been written to perform tasks which are usually regarded as requiring creativity in humans. We can derive some commonalities between these programs in order to build further creative programs. Key to this is the derivation of certain measures which assess how creative a program is. Starting from recent proposals by Ritchie, we define possible measures which describe the extent to which a program produces novel output. We discuss how this relates to the creativity of the program. |
Pease, Alison; Winterstein, Daniel; Colton, Simon Evaluating Machine Creativity Inproceedings In: Workshop on Creative Systems, 4th International Conference on Case Based Reasoning, pp. 129–137, 2001. @inproceedings{pease2001evaluating, title = {Evaluating Machine Creativity}, author = { Alison Pease and Daniel Winterstein and Simon Colton}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/10/pease_iccbr01.pdf}, year = {2001}, date = {2001-01-01}, booktitle = {Workshop on Creative Systems, 4th International Conference on Case Based Reasoning}, pages = {129--137}, abstract = {We consider relevant aspects of evaluating creativity to be input, output and the process by which the output is achieved. These issues may be further divided, and we highlight associated justifications and controversies. Appropriate methods of measuring these aspects are suggested and discussed.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We consider relevant aspects of evaluating creativity to be input, output and the process by which the output is achieved. These issues may be further divided, and we highlight associated justifications and controversies. Appropriate methods of measuring these aspects are suggested and discussed. |
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]. |
Pease, Alison; Lawrence, John; Budzynska, Katarzyna; Corneli, Joseph; Reed, Chris Lakatos-style Collaborative Mathematics through Dialectical, Structured and Abstract Argumentation Journal Article Forthcoming In: Artificial Intelligence, Forthcoming. @article{pease2017lakatos, title = {Lakatos-style Collaborative Mathematics through Dialectical, Structured and Abstract Argumentation}, author = {Alison Pease and John Lawrence and Katarzyna Budzynska and Joseph Corneli and Chris Reed }, journal = {Artificial Intelligence}, abstract = {The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. We demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. Finally, we offer reflections on our mixed-initiative collaborative approach. }, keywords = {}, pubstate = {forthcoming}, tppubtype = {article} } The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. We demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. Finally, we offer reflections on our mixed-initiative collaborative approach. |