Automatheo 2010 → Handout

Automatheo 2010

The 2010 Workshop on Automated Mathematical Theory Exploration
14-15 July 2010, Edinburgh, UK, a FLoC 2010 affiliated workshop of IJCAR and ITP.

Venue: ICMS at 14 India Street

View Larger Map








First Day: Wed 14 July 2010

TimeTitleAuthor(s)
09:15 - 09:45
TEA & REGISTRATION
09:45 - 10:00
Welcome and opening remarks
10:00 - 11:00
Theory Exploration and Duality in Geometry
Dana S. Scott
11:00 - 11:15
TEA & CHAT
11:15 - 11:45
The role of axiomatisation in mathematical discovery
Alison Pease
Dirk Schlimm has argued that the role of axiomatisation in mathematical discovery and the evolution of contemporary mathematics has been undervalued in philosophy of science and mathematics. We describe some examples of mathematical invention that illustrate evolution of axiomatisations in historical case studies, and argue that heuristics suggested by Lakatos in his rational reconstructions and Boden in her work on creativity can be used to describe some axiomatic development in mathematics. We will discuss a simple computational representation of some of these heuristics in a system based on Colton's HR program (our system is a work in progress). Our goal is to build a system which can take in a set of axioms in group theory, construct a theory from the axioms and evaluate the theory based on quality and difficulty, and then modify its axiom set by dropping, negating, or adding new axioms.
11:45 - 12:15
Theory Formation with HR and GC
John Charnley and Simon Colton
The HR automated theory formation system has been successfully applied to a number of mathematical and non-mathematical domains. HR uses several reasoning approaches in concert to form complex mathematical theories from the base axioms and concepts of a domain of investigation. We propose a demonstration of the system to illustrate how it is used and the types of theories it can generate. In addition, we will demonstrate a similar theory formation system, GC-ATF. This system applies a similar production-rule based concept generation technique to that of HR but has some notable differences. In particular, GC-ATF was created using a generic framework for combining reasoning systems that is based upon a cognitive architecture.
12:15 - 14:00
LUNCH
14:00 - 14:30
An Automated Confluence Proof for an Infinite Rewrite System via a Groebner Basis Computation
Loredana Tec
We outline a generic prototype implementation of the integro-differential polynomials modeling non-linear differential and integral expressions in one indeterminate function. The polynomials are designed and implemented using the generic functor language of the THEOREMA system. Our goal is to provide an automated proof for the confluence of a rewrite system for integro-differential operators corresponding to an infinitely generated noncommutative polynomial ideal.
14:30 - 15:00
Rewriting Completion Methods for Graphical Calculi
Lucas Dixon
In recent years, graphical calculi, based on monoidal categories or closely related structures, have been used to model computation in various forms. Examples include systems biology and quantum computation. These calculi are based on rewriting graphs. Graphical rewrites can be expressed as pairs of graphs and can also be used to rewrite each other. This raises an interesting possibility to adapt, and consider completion-based methods, such as Knuth-Bendix, that apply to these graphical rewrite systems. I will discuss adapting such completion methods for a particular formalism where edges describe the flow of data between primitive operations which are represented by vertices. These graphs have an interface made of half-edges (edges which have only one end connected to a vertex) and enjoy rich compositional principles by connecting graphs along these half-edges. One of the goals of this project is to help complete the development of a theory of quantum computation based on such graphical calculi.
15:00 - 15:30
Automating quantum interactions
Bob Coecke
Multipartite quantum entanglement is notoriously difficult to study; except for a zoo of proposed measures of entanglement there are hardly any structural insights. One exception are the so-called graph states of measurement based quantum computing. A compositional axiomatization for complementary observables was proposed [Coecke and Duncan ICALP 2008] which comprehends graph states, and Dixon, Duncan and Kissinger have produced a software tool which semi-automates reasoning with these [quantomatic http://dream.inf.ed.ac.uk/projects/quantomatic/]. Recently a more general compositional axiomatization for arbitrary multipartite qubit states has been proposed [Coecke and Kissinger ICALP 2010]. Given the hardness of studying these with traditional methods we expect that this area may be one were automation may produce original results which would have otherwise been very hard to obtain. There is currently a joint effort by researchers at Edinburgh and Oxford to tackle this problem.
15:30 - 16:00
TEA & CHAT
16:00 - 16:30
Theory exploration for working agebraists
David Stanovsky
As a working algebraist, I'd like to present a personal view on how automated theory exploration could possibly be used in research in algebra.
16:30 - 17:00
Dimensions and Challenges
Panel discussion
17:00 - late
DRINKS & CHAT & FOOD in nearby pub




Second Day: Thu 15 July 2010

TimeTitleAuthor(s)
09:30 - 10:00
TEA & REGISTRATION
10:00 - 11:00
Challenges in formalizing geometric theorems
John Harrison
11:00 - 11:15
TEA & CHAT
11:15 - 11:45
The Theory behind TheoryMine
Alan Bundy, Flaminia Cavallo, Lucas Dixon, Moa Johansson and Roy McCasland
We describe the technology behind the TheoryMine novelty gift company. A tower of four computer systems is used to generate recursive theories, then to speculate conjectures in those theories and then to prove these conjectures. All stages of the process are entirely automatic. The process guarantees large numbers of sound, novel theorems of some intrinsic merit.
11:45 - 12:15
Formalising Term Synthesis for IsaCoSy
Moa Johansson, Lucas Dixon and Alan Bundy
IsaCoSy is a theory formation system for inductive theories. It synthesise conjectures and use the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a formal account of the algorithms implemented in the system, and prove their correctness. In particular, we show that IsaCoSy only produces irreducible terms, using constraints generated from the left-hand sides of a set of rewrite rules.
12:15 - 14:00
LUNCH
14:00 - 14:30
Proof assistants in mathematics
Bogdan Grechuk
How can automated proof assistants actually help mathematicians in the nearest future? They can:
1) Guarantee proof correctness. But:
- How to be sure that the statement we formulated is actually "what we wanted to say"?
- How to be sure that there are no bugs inside a theorem prover?
- How to have a stable proof, valid forever?
2) Help us prove theorems. But:
- How to organize the library of proved results? How to search in such library?
- How to be able to use results proved in different provers?
- Can we use powerful tools, available in CAS, like Mathematica?
- We need new tactics: Proof by analogy. 3) Help us understand difficult proofs. But:
- What are realistic hopes in this direction?
14:30 - 15:00
Scheme-based Definition and Conjecture Synthesis for Inductive Theories
Omar Montano Rivas, Roy McCasland, Lucas Dixon and Alan Bundy
Human mathematical discovery processes include the invention of definitions, conjectures, theorems, examples, problems and algorithms for solving these problems. Automating these processes is an exciting area for research which is now recognised by the automated reasoning community. What is central to automated discovery programs is the generation of conjectures and definitions. Here we present a theory for mathematical theory exploration. The theory is grounded in a concept called scheme. A scheme is a higher-order formula intended to generate new definitions (definitional schemes) of the underlying theory and conjectures (propositional schemes) about them. The invention process is carried out through the instantiation of free variables within the scheme with closed terms of the theory.
Instantiated schemes are then normalized w.r.t. a normalizing term rewrite system R built from the defining equations of definitions and lemmata discovered during the exploration of the theory. Equivalent instantiations (modulo R) are identified by structural comparison of terms (up to variable renaming). The rewrite system R is not only used to reduce redundancies, inherent in most theory formation systems, but also to help with the proof obligations during the exploration of the theory. To asses the quality of the theorems discovered we perform a precision/recall analysis using Isabelle's theorem library as reference. We argue that the quality of a definition can be estimated by the number of theorems involving that definition at the end of the exploration process.
15:00 - 15:30
TEA & CHAT
15:30 - 16:00
Generating Examples
Roy McCasland
Quality examples play a very important role in mathematical theory exploration; they can contribute to research, not only by demonstrating that certain conjectures are false, but also by helping to guide researchers towards the truth. However, relatively little progress has thus far been achieved in automatically generating examples. This is unfortunate, because as things now stand, users must input by hand a significant amount of information that a 'good' automated theory exploration system should automatically produce. For instance, once a user has defined 'groups', a system ought to look over its database, and assuming it has the integers defined, together with plus, it should discover (without being prompted by the user) that this is indeed a group.
This talk will offer some suggestions about how one might automate the process of producing such examples - not necessarily from scratch, but from information previously supplied by the user. In particular, discovering the example of the integers being a group need not be all that difficult, provided one proceeds in stages. Presumably, prior to defining groups, the user will have defined 'binary operations', 'identities' and 'inverses' for these operations, and 'associative' operations. For each of these definitions, the system should discover that 'integer plus' fits the bill. In this way, by the time groups are defined, there is relatively little left for the system to do.
16:00 - 16:30
Dreams and Applications
Panel discussion
16:30 - 17:00
TEA & CHAT
17:00 - 19:00
Some business & DRINKS farewell to ICMS at India Street