sessions take place in auditorium 8.
||John Harrison, Intel, USA|
talk: Extracting test problems from real applications
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.
||Jürgen Zimmer, Saarland U, Germany|
Franke, Saarland U, Germany
Colton, U Edinburgh, UK
Sutcliffe, U Miami, USA
HR and tptp2X into MathWeb to compare automated theorem
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.