The Higher-Order Prover Leo-III (Extended Version)
From MaRDI portal
Publication:6297466
DOI10.1007/978-3-319-94205-6_8arXiv1802.02732MaRDI QIDQ6297466
Alexander Steen, Christoph Benzmüller
Publication date: 8 February 2018
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.
This page was built for publication: The Higher-Order Prover Leo-III (Extended Version)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6297466)
