Induction Challenge Management

Overview

Inductive Theorem proving is a small field. The main theorem provers within this field are Nqthm (now re-engineered as ACL2) [Boyer and Moore, 79, Kaufmann and Moore, 96], INKA [Autexier et. al, 99], the clam series [Bundy et. al, 90, Richardson et. al, 98] and RRL [Kapur and Zhang, 95]. Twelf [Pfenning and Schurmann, 99] 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 agreed 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.

In their present format these problems are 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. This means that the problems present a challenge not only to inductive theorem provers but to the emerging field of Mathematical Knowledge Management. This web page represents ongoing work at the University of Nottingham to provide systems to help manage these problems. This work has primarily been undertaken through the means of student projects.

Publications and Reports

T. D. Attfield, M. C. Duarte, L. Li, H.-Y. Mak, A. N. Neal, L. M. Toft, Z. Wang and L. A. Dennis, Induction Challenge OMDoc Manager (ICOM). Chapter 26 Applications and Projects, Section 11 in M. Kohlhase, OMDoc - An Open Markup Format for Mathematical Documents [version 1.2], Lecture Notes in Artificial Intelligence 4180, AI Systems Sub-Series. Springer, 2006. BibTex
T. D. Attfield, M. C. Duarte, L. Li, H.-Y. G. Mak, A. M. Neal, L. M. Toft and Z. Wang, OMDoc Manager, Unpublished Group Project Final Report, University of Nottingham, 2002.

People

Thomas David Attfield (Group Project Student 2001/2002, Individual Project 2002/2003)
Louise Dennis
Monica Cassandra Duarte (Group Project Student 2001/2002)
Lin Li (Group Project Student 2001/2002)
Ho-Ying Gloria Mak (Group Project Student 2001/2002)
Adam Michael Neal (Group Project Student 2001/2002)
Lewis Michael Toft (Group Project Student 2001/2002)
Zixuan Wang (Group Project Student 2001/2002)

Code and OMDoc Files

Sample OMDoc for the first challenge problem: IWC001a.omdoc
OMDoc Manager produced by 2001/2002 group project - this compiles (compile UI.java) under j2se 5.0.

Bibliography

Autexier et. al, 99: S. Autexier, D. Hutter, H. Mantel and A. Schairer, System description: INKA 5.0 - a logical voyager, in H. Ganzinger (ed), 16th International Conference on Automated Deduction, CADE-16. LNAI 1732, Springer, 1999.
Boyer and Moore, 79: R. S. Boyer and J S. Moore, A Computational Logic., ACM monograph series, Academic Press, New York, 1979
Bundy et. al, 90: Bundy, A. and van Harmelen, F. and Horn, C. and Smaill, A., The Oyster-Clam system, in M. E. Stickel (ed), 10th International Conference on Automated Deduction, pp. 647-648, LNAI 449, Springer, 1990.
Kapur and Zhang, 95: D. Kapur and H. Zhang, An overview of Rewrite Rule Laboratory (RRL), J. Computer and Mathematics with Applications, 1995, 29 2, pp. 91-114
Kaufmann and Moore, 96: M. Kaufmann and J S. Moore, ACL2: An Industrial Strength Version of Nqthm, Compass'96: Eleventh Annual Conference on Computer Assurance, 1996.
Pfenning and Schurmann, 99: F. Pfenning and C. Schurmann, System Description: Twelf --- {A} Meta-Logical Framework for Deductive Systems, in H. Ganzinger (ed), Proceedings of the 16th International Conference on Automated Deduction (CADE-16), LNAI 1632, pp. 202-206, Springer, 1999.
Richardson et. al, 98: J.D.C. Richardson, A. Smaill and I. Green, System Description: Proof Planning in Higher-Order Logic with Lambda-Clam, in C. Kirchner and H. Kirchner (eds), Conference on Automated Deduction (CADE'98), LNCS 1421, pp. 129-133, Springer, 1998.