Automatheo 2010 → Handout

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

14-15 July 2010, Edinburgh, UK, a FLoC 2010 affiliated workshop of IJCAR and ITP.

Venue: ICMS at 14 India Street

View Larger Map

**Getting to the ICMS**Note that this is not the same location as other FLoC events, and it takes about 30 minutes to walk (or 10 minutes by bus) between sites.

the Lothian bus route map is not very good, but is still the best overview of busses in Edinburgh.

**from Appleton Tower and the Informatics Forum:**The bus number 42 passes along Buccleuch Street, right by the Informatics Forum and Appleton tower, but only runs every 30 minutes. See the google map with stops and live bus tracker for the bus number 42.You can also catch the number 29, from Nicholson Street, which runs every 15 minutes. See the google map with stops and live bus tracker for the bus number 29.

For either bus, one should get off just past Herriot Row, then walk west along Herriot Row for one block -- India Street will be the first right. They can have a look at the ICMS web page map

A Taxi from Appleton Tower will cost around 7 pounds.

TimeTitleAuthor(s)

TEA & REGISTRATION

Welcome and opening remarks

Theory Exploration and Duality in Geometry

TEA & CHAT

The role of axiomatisation in mathematical discovery

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.

Theory Formation with HR and GC

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.

LUNCH

An Automated Confluence Proof for an Infinite Rewrite System via a Groebner Basis Computation

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.

Rewriting Completion Methods for Graphical Calculi

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.

Automating quantum interactions

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.

TEA & CHAT

Theory exploration for working agebraists

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.

Dimensions and Challenges

DRINKS & CHAT & FOOD in nearby pub

TimeTitleAuthor(s)

TEA & REGISTRATION

Challenges in formalizing geometric theorems

TEA & CHAT

The Theory behind TheoryMine

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.

Formalising Term Synthesis for IsaCoSy

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.

LUNCH

Proof assistants in mathematics

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?

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?

Scheme-based Definition and Conjecture Synthesis for Inductive Theories

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.

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.

TEA & CHAT

Generating Examples

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.

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.

Dreams and Applications

TEA & CHAT

Some business & DRINKS farewell to ICMS at India Street