The Higher-Order Prover Leo-III (Extended Version)

February 08, 2018 Β· Declared Dead Β· πŸ› 9th International Joint Conference on Automated Reasoning, IJCAR 2018, Oxford, UK, July 14-17, 2018, Proceedings, Springer

πŸ‘» CAUSE OF DEATH: Ghosted
No code link whatsoever

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Alexander Steen, Christoph BenzmΓΌller arXiv ID 1802.02732 Category cs.AI: Artificial Intelligence Cross-listed cs.LO, math.LO Citations 0 Venue 9th International Joint Conference on Automated Reasoning, IJCAR 2018, Oxford, UK, July 14-17, 2018, Proceedings, Springer Last Checked 4 months ago
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.
Community shame:
Not yet rated
πŸ“„ View on arXiv 🌐 View on ar5iv πŸ“‘ PDF πŸŽ‰ Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

πŸ“œ Similar Papers

In the same crypt β€” Artificial Intelligence

Died the same way β€” πŸ‘» Ghosted