System Description: LEO -- A Resolution based Higher-Order Theorem Prover
Christoph Benzmüller · 2005
We present Leo, a resolution based theorem prover for classical higher-order logic. It can be employed as both an fully automated theorem prover and an interactive theorem prover. Leo has been implemented as part of the Ωmega environment [23] and has been integrated with the Ωmega proof assistant. Higher-order resolution proofs developed with Leo can be displayed and communicated to the user via Ωmega’s graphical user interface Loui. The Leo system has recently been successfully coupled with a first-order resolution theorem prover (Bliksem).