[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS] Announcement of LEO-II
(please apologize multiple e-mails)
- 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