The higher-order prover Leo-III
From MaRDI portal
Publication:1799072
DOI10.1007/978-3-319-94205-6_8OpenAlexW2886133399MaRDI QIDQ1799072
Alexander Steen, Christoph Benzmüller
Publication date: 18 October 2018
Full work available at URL: https://arxiv.org/abs/1802.02732
Related Items (23)
Improving automation for higher-order proof steps ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ A Polymorphic Vampire ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Unnamed Item ⋮ The MET: The Art of Flexible Reasoning with Modalities ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Superposition for higher-order logic ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Superposition with lambdas ⋮ Efficient local reductions to basic modal logic ⋮ Superposition for full higher-order logic ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ GRUNGE: a grand unified ATP challenge ⋮ Leo-III ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Local reductions for the modal cube
Uses Software
This page was built for publication: The higher-order prover Leo-III
