[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] 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