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.

• Louise Dennis, University of Edinburgh
• Dieter Hutter, DFKI

001 - Arithmetic Geometric Mean

1. First Order Version of the Arithmetic/Geometric Mean
2. Higher Order Version of the Arithmetic/Geometric Mean (Version 1)
3. 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

1. Rotate Length (Version I)
2. Rotate Length (Version II)

005 - Binomial Theorems

1. Binomial Theorems (Version I)
2. Binomial Theorems (Version II)

006 - Two definition of Even are equivalent

007 - All numbers are odd or even

008 - Chinese Remainder Theorem

1. Chinese Remainder Theorem (Version I)
2. Chinese Remainder Theorem (Version II)
3. Chinese Remainder Theorem (Higher-order)

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)