Challenges
This collection of challenging examples has been assembled for researchers
who are working on inductive theorem provers for the purpose of
provoding a body of test examples. The description of the
example problems is purposely kept informal, in order
not to intervene with the representation of a problem in a particular
theorem prover.
Major contributions to this corpus have come from
 Louise Dennis, University of Edinburgh
 Dieter Hutter, DFKI
If you want to contribute to the corpus, please send mail to
Carsten Schuermann. New additions
will be annouced on the challenges mailing list. You may
subscribe to the mailing list by sending email to
majordomo@twelf.org
with "subscribe challenge" in the body (the header might stay empty).
Everybody is invited to submit challenges.
001  Arithmetic Geometric Mean
 First Order Version of the Arithmetic/Geometric Mean
 Higher Order Version of the Arithmetic/Geometric Mean (Version 1)
 Higher Order Version of the Arithmetic/Geometric Mean (Version 2)
002  Length of the joined list of two lists of even length is even
003  A member of a list is a member of that list joined to another
004  Rotate Length
 Rotate Length (Version I)
 Rotate Length (Version II)
005  Binomial Theorems
 Binomial Theorems (Version I)
 Binomial Theorems (Version II)
006  Two definition of Even are equivalent
007  All numbers are odd or even
008  Chinese Remainder Theorem
 Chinese Remainder Theorem (Version I)
 Chinese Remainder Theorem (Version II)
 Chinese Remainder Theorem (Higherorder)
009  "Pete's Nasty Theorem"
010  Quicksort
011  Safety Lemma for Removing the head of an abstract list
012  Safety Lemma for Prefix Operation
013  Divide and Conquer
014  Harald's Problem
015  Paulson's Problem
016  Quicksort verification
017  Verifying Abstractions in Model Checking (revised)
