[FOM] Automated Reasoning Challenge

[by way of Martin Davis <martin@eipye.com>]

Hi Martin,

The MPTP $100 Challenges are sets of classical first-order reasoning problems,
expressed in the TPTP language, to be proved by fully automated reasoning
systems, within specified reasonable resource constraints. The challenge
problems are based on the Mizar Mathematical Library. The goal of the MPTP
challenges is to boost the development of automated theorem proving and
artificial intelligence methods and tools for reasoning in large theories that
involve large numbers of consistently used concepts. Details of the challenges,
including instructions for entering, are available at ...
     http://www.tptp.org/MPTPChallenge/

The winners of the MPTP challenges will be announced at CADE-21, and will each
receive $100 in real US dollars ... who says there's no money in ATP! Results
on the challenge problems, for publicly available systems, are on the web page.
If your browser is up to it, the interactive interface is fun to use :-)

Cheers,

Josef (Urban) and Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264
----- "My cat" is not a float. Every string should learn to swim. ------