The Higher-Order Prover Leo-III (Extended Version)
Artificial Intelligence
2018-04-20 v2 Logic in Computer Science
Logic
Abstract
The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF, TFF, THF), including their recent extensions to rank-1 polymorphism (TF1, TH1). In addition, the prover natively supports almost every normal higher-order modal logic. Leo-III cooperates with first-order reasoning tools using translations to many-sorted first-order logic and produces verifiable proof certificates. The prover is evaluated on heterogeneous benchmark sets.
Keywords
Cite
@article{arxiv.1802.02732,
title = {The Higher-Order Prover Leo-III (Extended Version)},
author = {Alexander Steen and Christoph Benzmüller},
journal= {arXiv preprint arXiv:1802.02732},
year = {2018}
}
Comments
13 pages (this is an extended version of the IJCAR 2018 paper)