siglauvt2.jpg synasc2006.jpg
 Main Menu
Call for papers
ACSys workshop
GridCAD workshop
ICS workshop
MTE workshop
NCA workshop
PN&WM workshop
Invited talks
Important dates
Social programme
Registration form
Contact info
Previous editions

Synasc 2006 - Abstract_Buchberger PDF Print

Also, in this process of mathematical theory exploration,  storage and retrieval of knowledge plays an important role. The way how one proceeds in building up a mathematical theory in successive,  well structured, layers has significant influence on the ease of proving individual propositions that occur in the build-up of the theory and also on the readability and explanatory power of the proofs  generated. Furthermore, in the practice of mathematical theory  exploration, different reasoning methods  are used for different  theories and, in fact, reasoning methods are expanded and changed in  the process of exploring theories, whereas traditional automated reasoning  systems try to get along with one reasoning method for  large parts or all of mathematics.

We describe a methodology for the algorithmic support of mathematical theory exploration. Starting from any mathematical knowledge base  (collection of formulae that may be axioms, definitions,  propositions, lemmas, theorems, problem specifications, algorithms),  in one exploration round, we introduce  a few new notions by axioms or definitions and then explore the possible interactions of these notions with all existing notions as completely as possible before we  proceed to the introduction of the next notions. Achieving a certain  degree of completeness in the current exploration round  is crucial  for decreasing the complexity of proving in the subsequent exploration rounds.

The invention of axioms and definitions, the invention of propositions that describe interactions between notions, the invention of problems involving the new notions, and the  invention of algorithms that solve these problems is something which,  typically, needs a certain degree of human intervention. However, we
show that significant algorithmic support for these invention steps  is possible by the use of  {\em formula schemes}. Formula schemes are formulae with higher order variables for functions and predicates
 that describe fundamental properties of functions and predicates, as for example commutativity, isomorphy,  etc., that have proved to be  useful in the practice of mathematics.

The application of formula schemes provides a kind of bottom-up  support in the exploration of mathematical theories. A second idea is orthogonal to the use of formula schemes and provides top-down
support in the exploration:  We provide tools for the analysis of  failing proofs.

 Failing proofs contain a lot of creative information. They give us hints about missing links in the systematic exploration of notions. For example, a failing induction proof  of a conjecture may give us a  hint about which lemmas we should try to prove before going back to the proof of the conjecture. The extraction of intermediate lemmas from failing proofs can, however, also be applied for the synthesis of algorithms.

We illustrate  the interplay between the use of formula schemes,  lemma extraction from failing proofs and automated reasoning (special reasoners for special theories) in a couple of examples. Our main example is the theory of Groebner bases that has found numerous applications in many different areas of mathematics (algebraic  geometry, symbolic analysis, algebraic combinatorics etc.).  Particular emphasis is put on a new method for the algorithm-supported synthesis of algorithms,  which we call lazy thinking method, that combines the use of formula schemes and the  extraction of conjectures from failing (automated) proofs in a specific way:

 Our algorithm synthesis method is strong enough, for example, to  automatically synthesize an algorithm for the construction of Groebner bases. This is surprising because the construction of Groebner bases is a  completely nontrivial problem which - in the early days of computer  algebra - was even conjectured to be algorithmically unsolvable. We also  give some remarks, again in the example of Groebner bases theory, on the use of special theorem provers and the expansion and change of provers during the process of  mathematical theory exploration and the implications of these facts on future reasoning  systems for mathematics. All the examples are given in our Theorema system, which tries to  implement the  above approach to mathematical theory exploration.


Copyright(C) 2006 - Department of Computer Science, email: