Induction Challenge Problems

Inductive Theorem proving is a small field. The main theorem provers within this field are Nqthm (now re-engineered as ACL2), INKA, the clam series and RRL. Twelf also looks at the automation of inductive proof inthe context of logical frameworks. Within the field it is hard to assess claims for the superiority of any given system since there is naturally a tendency to report "successes" - difficult or challenging problems automatically proved. There is also a desire within the community to develop a store of shared knowledge about the challenges that face the automation of proof by mathematical induction.

TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for first-order ATP systems. They provide the ATP community with a comprehensive library complete with unambiguous names and references. All the problems are stated in a standardised formulation of first-order logic and are widely used to benchmark first-order systems. They are also used as the test set for the CASC competition which compares such systems. One of the benefits of the TPTP library to the ATP community is the existence of a common set of problems by which comparisons can be made.

It is not practical for inductive theorem provers to follow the pattern of the TPTP library. Various attempts have been made to build a similar corpus of problems requiring inductive reasoning. The most mature of these was based on the Boyer-Moore corpus (This has become known as the Dmac corpus after David McAllester who translated a fragment of the NQTHM corpus into a simpler language.). This corpus was unpopular partly because there was repetition within the problem set and partly because many problems depended on a few particular function definitions. But the major objection was that inductive theorem provers use a number of different logics, some of which are typed and some of which are not, which made it difficult to agree on a standard format. The use of other logics also raised translation issues and a fully automated process for converting the theorems, even into an agreed typed language was never produced.

A group of researchers within the community (At the 2000 CADE Workshop on the Automation of Proof by Mathematical Induction.) agreed that instead of a large set of benchmarks in a standard logic they would each put forward a number of "Challenge Problems". These should present interesting challenges to the automation of inductive proof or illustrate important features which an inductive prover should be able to handle. A set of these problems would be collected which would remain sufficiently small that an individual could represent them within their own theorem proving system as they saw fit.

This web page represents the current status of these challenge problems. They described in a high-level way and written up in an ad hoc fashion. The descriptions contain both mathematical notation and commentary. They are difficult to read, navigate or use in any particular system. Work is in progress to build systems to standardize the presentation and aid navigation.

The Challenges (in Plain Text and TPTP Typed Higher Order Form)

Publications

Projects Involving the Challenge Problems

If you are using the induction challenge problems please contact Louise Dennis.

Louise Dennis
Last modified: Sun Oct 5 10:20:45 BST 2008