Email Gateway (Aug 18 2022 at 11:09): Email Gateway (Aug 18 2022 at 11:09):From: Lawrence Paulson <lp15@cam.ac.uk>
(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
Last updated: May 03 2024 at 01:09 UTC