RADM on Wednesday

Detailed program
Wednesday July 31st, 2002
See also the unified by-slot program

All sessions take place in auditorium 8.

Session 1

09:00-09:30  Paul Cairns, U College London, UK
Jeremy Gow, U College London, UK
Automated deduction systems for real mathematicians

09:30-10:00  Chen Lingjun, Nihon U, Japan
Hidetsune Kobayashi, Nihon U, Japan
Hirokazu Murao, U Electro-Communications, Japan
Hideo Suzuki, Polytechnic U, Japan
Notes on formalizing induction on the number of sets

10:00-10:30  Simon Colton, U Edinburgh, UK
Roy McCasland, U Edinburgh, UK
Alan Bundy, U Edinburgh, UK
Toby Walsh, U College Cork, Ireland
Automated theory formation for tutoring tasks in pure mathematics

Session 2

11:00-11:30  Manfred Kerber, U Birmingham, UK
Martin Pollet, Saarland U, Germany
On the design of mathematical concepts

11:30-12:00  Christoph Schwarzweller, U Tübingen, Germany
Symbolic deduction in mathematical databases based on properties

Joint session 1

Joint with PaPS

14:00-15:00  John Harrison, Intel, USA
Invited talk: Extracting test problems from real applications
The HOL Light theorem prover has a number of automated subsystems, e.g., a model elimination procedure for first order logic with equality, and arithmetic provers for linear and non-linear arithmetic. The sub-problems that are dealt with by these components can easily be extracted to give a good selection of the relatively easily decidable problems that arise in "real" applications, such as formalizing mathematics and performing industrial verifications. These can then be used as test problems for other automated provers, and possibly incorporated into standard test suites such as TPTP. We have already made available some test problems generated in this way.
This simple approach has the disadvantage that the problems tend to be relatively easy, and self-selected for the particular methods used in HOL's own provers. However, since HOL is an LCF-style prover, it is essentially trivial to capture all proofs in the system, regardless of whether they are wholly or partly automated. Using this technique, we can generate realistic test problems of essentially arbitrary difficulty.

15:00-15:30  Jürgen Zimmer, Saarland U, Germany
Andreas Franke, Saarland U, Germany
Simon Colton, U Edinburgh, UK
Geoff Sutcliffe, U Miami, USA
Integrating HR and tptp2X into MathWeb to compare automated theorem provers
The assessment and comparison of automated theorem proving systems (ATPs) is important for the advancement of the field. At present, the de facto assessment method is to test provers on the TPTP library of nearly 6000 theorems. We describe here a project which aims to complement the TPTP service by automatically generating theorems of sufficient difficulty to provide a significant test for first order provers. This has been achieved by integrating the HR automated theory formation program into the MathWeb Software Bus. HR generates first order conjectures in TPTP format and passes them to a concurrent ATP service in MathWeb. MathWeb then uses the tptp2X utility to translate the conjectures into the input format of a set of provers. In this way, various ATP systems can be compared on their performance over sets of thousands of theorems they have not been previously exposed to. Our purpose here is to describe the integration of various new programs into the MathWeb architecture, rather than to present a full analysis of the performance of theorem provers. However, to demonstrate the potential of the combination of the systems, we describe some preliminary results from experiments in group theory.

Joint session 2

Joint with PaPS

16:00-17:30  Peter B. Andrews, Carnegie Mellon U, USA
Alan Bundy, U Edinburgh, UK
William McCune, Argonne National Laboratory, USA
Rick Sommer, Stanford U, USA
Panel: Challenge problems for automated deduction (with special emphasis on mathematics)