FLoC '02 - PaPS Wednesday July 31st

PaPS on Wednesday

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

All sessions take place in auditorium 8.

Joint session 1

Joint with RADM

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 RADM

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)