John Charnley
Research Associate
About me
I am a research associate in the group, working on the Computational Creativity Theory project. I study methods for creating combined reasoning systems. These are systems that use a variety of Artificial Intelligence approaches in combination. In particular, I’m investigating how models of human cognition can be used as a basis for these systems and how they might be applied to domains such as mathematical discovery, constraint solving and machine learning.
I previously worked on a knowledge transfer project, in partnership with Lionhead Studios. The project looked at applications of AI techniques to GUI design for the Microsoft Kinect controller.
Publications
Llano, Maria Teresa; Hepworth, Rose; Colton, Simon; Gow, Jeremy; Charnley, John; Lavrač, Nada; Žnidaršič, Martin; Perovšek, Matic; Granroth-Wilding, Mark; Clark, Stephen Baseline Methods For Automated Fictional Ideation Inproceedings In: Proceedings of the 5th international conference on computational creativity, 2014. @inproceedings{llano2014baseline, title = {Baseline Methods For Automated Fictional Ideation}, author = { Maria Teresa Llano and Rose Hepworth and Simon Colton and Jeremy Gow and John Charnley and Nada Lavrač and Martin Žnidaršič and Matic Perovšek and Mark Granroth-Wilding and Stephen Clark}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/09/llano_iccc2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the 5th international conference on computational creativity}, abstract = {The invention of fictional ideas (ideation) is often a central process in the creative production of artefacts such as po- ems, music and paintings, but has barely been studied in the Computational Creativity community. We present here three baseline approaches for automated fictional ideation, using methods which invert and alter facts from the ConceptNet and ReVerb databases, and perform bisociative discovery. For each method, we present a curation analysis, by calculating the proportion of ideas which pass a typicality evaluation. We further evaluate one ideation approach through a crowd- sourcing experiment in which participants were asked to rank ideas. The results from this study, and the baseline meth- ods and methodologies presented here, constitute a firm basis on which to build more sophisticated models for automated ideation with evaluative capacity.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The invention of fictional ideas (ideation) is often a central process in the creative production of artefacts such as po- ems, music and paintings, but has barely been studied in the Computational Creativity community. We present here three baseline approaches for automated fictional ideation, using methods which invert and alter facts from the ConceptNet and ReVerb databases, and perform bisociative discovery. For each method, we present a curation analysis, by calculating the proportion of ideas which pass a typicality evaluation. We further evaluate one ideation approach through a crowd- sourcing experiment in which participants were asked to rank ideas. The results from this study, and the baseline meth- ods and methodologies presented here, constitute a firm basis on which to build more sophisticated models for automated ideation with evaluative capacity. |
Llano, Maria Teresa; Hepworth, Rose; Colton, Simon; Charnley, John; Gow, Jeremy Automating Fictional Ideation Using ConceptNet Inproceedings In: Proceedings of the AISB14 symposium on computational creativity, 2014. @inproceedings{llano2014automating, title = {Automating Fictional Ideation Using ConceptNet}, author = {Maria Teresa Llano and Rose Hepworth and Simon Colton and John Charnley and Jeremy Gow}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/09/llano_aisb14.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the AISB14 symposium on computational creativity}, abstract = {The invention of fictional ideas (ideation) is often a cen- tral process in producing artefacts such as poems, music and paint- ings in a creative way. Automated fictional ideation should, there- fore, be of much interest in the study of Computational Creativity, but only a few approaches have been explored. We describe here the preliminary results of a new method for automated generation and evaluation of fictional ideas which uses ConceptNet, a semantic net- work. We evaluate the results obtained through a small study that involves participants scoring ideas via an online survey. We believe this approach constitutes a firm basis on which a more sophisticated model for automated creative ideation can be built.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } The invention of fictional ideas (ideation) is often a cen- tral process in producing artefacts such as poems, music and paint- ings in a creative way. Automated fictional ideation should, there- fore, be of much interest in the study of Computational Creativity, but only a few approaches have been explored. We describe here the preliminary results of a new method for automated generation and evaluation of fictional ideas which uses ConceptNet, a semantic net- work. We evaluate the results obtained through a small study that involves participants scoring ideas via an online survey. We believe this approach constitutes a firm basis on which a more sophisticated model for automated creative ideation can be built. |
Charnley, John; Colton, Simon; Llano, Maria Teresa The FloWr Framework: Automated Flowchart Construction, Optimisation and Alteration for Creative Systems Inproceedings In: Proceedings of the 5th international conference on computational creativity, 2014. @inproceedings{charnley2014flowr, title = {The FloWr Framework: Automated Flowchart Construction, Optimisation and Alteration for Creative Systems}, author = { John Charnley and Simon Colton and Maria Teresa Llano}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/08/charnley_iccc2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the 5th international conference on computational creativity}, volume = {9}, abstract = {We describe the FloWr framework for implementing creative systems as scripts over processes and manipulated visually as flowcharts. FloWr has been specifically developed to be able to automatically optimise, alter and ultimately generate novel flowcharts, thus innovating at process level. We describe the fundamental architecture of the framework and provide ex- amples of creative systems which have been implemented in FloWr. Via some preliminary experimentation, we demon- strate how FloWr can optimise a given system for efficiency and yield, alter input parameters to increase unexpectedness, and build novel generative systems automatically.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We describe the FloWr framework for implementing creative systems as scripts over processes and manipulated visually as flowcharts. FloWr has been specifically developed to be able to automatically optimise, alter and ultimately generate novel flowcharts, thus innovating at process level. We describe the fundamental architecture of the framework and provide ex- amples of creative systems which have been implemented in FloWr. Via some preliminary experimentation, we demon- strate how FloWr can optimise a given system for efficiency and yield, alter input parameters to increase unexpectedness, and build novel generative systems automatically. |
Colton, Simon; Charnley, John Towards a Flowcharting System for Automated Process Invention Inproceedings In: Demo session Proceedings of the 4th International Conference on Computational Creativity, 2013. @inproceedings{Colton2013ICCC, title = {Towards a Flowcharting System for Automated Process Invention}, author = {Simon Colton and John Charnley}, url = {http://ccg.doc.gold.ac.uk/wp-content/uploads/2016/11/colton_icccdemo13.pdf}, year = {2013}, date = {2013-11-01}, booktitle = {Demo session Proceedings of the 4th International Conference on Computational Creativity}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } |
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. |
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. |
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. |
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. |
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. |
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. |
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 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. |
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. |