Content Tags

There are no tags.

The Higher-Order Prover Leo-III.

RSS Source
Alexander Steen, Christoph Benzmüller

The automated theorem prover Leo-III for classical higher-order logic withHenkin semantics and choice is presented. Leo-III is based on extensionalhigher-order paramodulation and accepts every common TPTP dialect (FOF, TFF,THF), including their recent extensions to rank-1 polymorphism (TF1, TH1). Inaddition, the prover natively supports almost every normal higher-order modallogic. Leo-III cooperates with first-order reasoning tools using translationsto (polymorphic) many-sorted first-order logic and produces verifiable proofcertificates. The prover is evaluated on heterogeneous benchmark sets.

Stay in the loop.

Subscribe to our newsletter for a weekly update on the latest podcast, news, events, and jobs postings.