The higher-order prover Leo-III

DOI10.1007/978-3-319-94205-6_8OpenAlexW2886133399MaRDI QIDQ1799072FDOQ1799072

Authors: Alexander Steen, Christoph Benzmüller 

Publication date: 18 October 2018

Full work available at URL: https://arxiv.org/abs/1802.02732

Recommendations

• The higher-order prover \textsc{Leo}-II
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Extensional paramodulation for higher-order logic and its effective implementation Leo-III
• A verified proof checker for higher-order logic
• Higher-order quantification and proof search
• Proof-theoretic and higher-order extensions of logic programming
• scientific article; zbMATH DE number 1552534
• scientific article; zbMATH DE number 638309

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (28)

• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Restricted combinatory unification
• SAT-Inspired Higher-Order Eliminations
• Solving modal logic problems by translation to higher-order logic
• Superposition with lambdas
• Local reductions for the modal cube
• Improving automation for higher-order proof steps
• Extensional higher-order paramodulation in Leo-III
• The MET: The Art of Flexible Reasoning with Modalities
• Title not available (Why is that?)
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Making higher-order superposition work
• Superposition with lambdas
• A combinator-based superposition calculus for higher-order logic
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• Superposition for higher-order logic
• Title not available (Why is that?)
• GRUNGE: a grand unified ATP challenge
• Leo-III
• Efficient local reductions to basic modal logic
• Superposition for full higher-order logic
• The Lean 4 theorem prover and programming language
• Superposition with Delayed Unification
• Extending SMT solvers to higher-order logic
• Practical Proof Search for Coq by Type Inhabitation
• Translating SUMO-K to Higher-Order Set Theory
• A Polymorphic Vampire
• The Higher-Order Prover Leo-III (Extended Version)

Uses Software

• Isabelle/HOL
• TPTP
• Satallax
• QMLTP
• MetTeL
• LeoPARD
• MSPASS
• MleanCoP

This page was built for publication: The higher-order prover Leo-III

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799072)