Tech Reports

ULCS-07-004

Challenge Problems for Inductive Theorem Provers v1.0

Louise A. Dennis, Jeremy Gow and Carsten Shurmann


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 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.

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 problem set.

[Full Paper]