[isabelle] Announcement of LEO-II

(please apologize multiple e-mails)

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


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

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.