Leo-III Version 1.1 (System description) | Zendy

Christoph Benzmüller | Zendy; Alexander Steen | Zendy; Max Wisniewski | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Leo-III Version 1.1 (System description)

Author(s) -

Christoph Benzmüller,

Alexander Steen,

Max Wisniewski

Publication year - 2018

Publication title -

kalpa publications in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 2515-1762

DOI - 10.29007/grmx

Subject(s) - automated theorem proving , sketch , computer science , scheme (mathematics) , order (exchange) , programming language , gas meter prover , calculus (dental) , asynchronous communication , rank (graph theory) , theoretical computer science , algebra over a field , algorithm , mathematics , combinatorics , pure mathematics , medicine , mathematical analysis , computer network , geometry , dentistry , finance , mathematical proof , economics

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external firstorder theorem provers. Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III’s underlying calculus, survey implementation details and give examples of use.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research