Title: Challenge Problems for Inductive Theorem Provers v1.0
Abstract: Within the field of inductive theorem proving it is hard to assess claims for the superiority of any given system since there is naturally a tendency to report “successes” ‐ difficult or c hallenging 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. A group of researchers within the community agreed that 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. This technical report represent the current state of this challenge pro blem set. Inductive Theorem proving is a small field. The main theorem p rovers within this field are Nqthm [2] (now reengineered as ACL2 [6]), INKA [1], the Clam series [4, 8] and RRL [5]. Twelf [7] also looks at the automation of inductive proof in the 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) [10] 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 firstorder systems. They are also used as the test set for the CASC competition [9] which compares such systems. One of the benefits of the TPTP library to the ATP community is the e xistence of a common set of problems by which comparisons can be made. It is not practical for inductive theorem provers to follow t he 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 [2] corpus 1 . 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 o f 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 2 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 feat ures which an inductive prover should be able to handle. A set of these problems would be collected which would remain suffi ciently small that an individual could represent them within their own theorem proving system as they saw fit. This technical report represent the current state of this ch allenge problem set.
Publication Year: 2007
Publication Date: 2007-01-01
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot