Search
 
loader loading subjects...
cover
The Higher-Order Prover Leo-III
Alexander Steen, Christoph Benzmüller
2937 - 2938
10.3233/FAIA200462
Research Article
Frontiers in Artificial Intelligence and Applications
Volume 325: ECAI 2020
Abstract

Leo-III is an effective automated theorem prover for extensional type theory with Henkin semantics. It is based on an extensional higher-order paramodulation calculus and supports reasoning in monomorphic and rank-1 polymorphic first-order and higher-order logics. Leo-III also automates various non-classical logics, including almost every normal higher-order modal logic.

Download
Creative Commons License