LEO II: An Effective Higher-Order Theorem Prover
Lead Research Organisation:
University of Cambridge
Department Name: Computer Science and Technology
Abstract
An Automatic Theorem Prover (ATP) is a piece of software that can prove mathematical statements automatically. Modern ATPs are impressively powerful, often coping with problems that involve thousands of separate facts. ATPs can be applied to practical tasks such as finding faults in computer programs. In general, the use of mathematical logic to analyse computer designs is called formal verification.One limitation of most ATPs concerns the language in which the mathematical statements are expressed. Most ATPs accept first-order logic, which can express assertions about individual items, as in all integers are either even or odd . However, many statements in mathematics are difficult to express in first-order logic, especially if they refer to sets or functions.Higher-order logic resembles first-order logic, but it has built-in notions of sets and functions. It is widely used in formal verification, being especially convenient for expressing assertions about computer hardware designs. Unfortunately, there is only one ATP for higher-order logic; it dates from the 1980s and its performance is poor by modern standards. An experimental higher-order ATP, called LEO, has recently shown promise; in recent work, it has been combined with a conventional ATP so that it can benefit from the latter's high performance.The proposal is to take the ideas recently prototyped in LEO and use them as the basis for a robust new higher-order ATP. It is intended for applications in formal verification, but the project will also shed light on fundamental issues in the mechanization of higher-order logic.
Organisations
Publications
Benzmueller C
(2010)
Multimodal and intuitionistic logics in simple type theory
in Logic Journal of IGPL
Benzmüller C
(2012)
Quantified Multimodal Logics in Simple Type Theory
in Logica Universalis
Benzmüller C
(2013)
Logic for Programming, Artificial Intelligence, and Reasoning
Benzmüller C
(2010)
Computational Logic in Multi-Agent Systems
Benzmüller C
(2015)
The Higher-Order Prover Leo-II.
in Journal of automated reasoning
Benzmüller C
(2008)
Combined reasoning by automated cooperation
in Journal of Applied Logic
Benzmüller C
(2010)
Verification, Induction, Termination Analysis
Benzmüller C
(2011)
Combining and automating classical and non-classical logics in classical higher-order logics
in Annals of Mathematics and Artificial Intelligence
Benzmüller C
(2012)
Higher-order aspects and context in SUMO
in Journal of Web Semantics
Description | The purpose of this project was to investigate some new ideas for implementing an advanced automatic theorem prover for higher-order logic. Over the course of the year that this project ran, the basic architecture was designed and the theorem prover, entitled LEO-II, was delivered. The appropriateness of this architecture is demonstrated by the high performance of LEO-II compared with other systems of its general type. The key idea is cooperation between systems: LEO-II deals with higher-order elements of a given problem, attempting to reduce it to a first-order problem, whose solution of delegates to an external first-order theorem prover. |
Exploitation Route | This is basic work, but Benzmüller has used LEO-II for many investigations involving formal logical systems. Recent research has been aimed at preparing LEO-II for integration with Isabelle's highly successful Sledgehammer tool. |
Sectors | Digital/Communication/Information Technologies (including Software) |
URL | http://www.cl.cam.ac.uk/~lp15/Grants/LEO-II/ |
Title | LEO-II |
Description | LEO-II is an automatic theorem prover for higher-order logic. That means, it can be given statements expressed in mathematical notation and it attempts to prove them. Higher-order logic is a mathematical language with built-in support for sets and functions. |
Type Of Technology | Software |
Year Produced | 2008 |
Open Source License? | Yes |
Impact | Used in various studies concerning modal logic and even a proof of the existence of God. |
URL | http://page.mi.fu-berlin.de/cbenzmueller/leo/ |