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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.