The Coq mailing list

[Christoph Benzmueller <chris AT ags.uni-sb.de>]

(please apologize multiple e-mails)

========================================================
                   Announcement of
                     - LEO-II -
   An automated theorem prover for higher-order logic

        http://www.ags.uni-sb.de/~chris/leo/
========================================================

LEO-II is a standalone, resolution-based higher-order
theorem prover designed for effective cooperation with
specialist provers for natural fragments of higher-order
logic such as first-order and propositional logic.
Currently LEO-II cooperates with the first-order
automated theorem provers E, SPASS, and Vampire.
LEO-II comes with an automatic and an interactive
mode.

LEO-II is implemented in Objective Caml and its
problem representation language is TPTP THF.
The distribution contains approx. 70 example problems
encoded in TPTP THF syntax.

The development of LEO-II has been supported by the
EPSRC grant EP/D070511/1 at Cambridge University.
The people behind the LEO-II system are:
C. Benzmueller, L. Paulson, A. Fietzke and F. Theiss
from Cambridge University and Saarland University.

Dec 16, 2007
                                 Christoph Benzmueller