Superposition for \(\lambda\)-free higher-order logic

DOI10.1007/978-3-319-94205-6_3OpenAlexW2810826868MaRDI QIDQ1799065

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann

Publication date: 18 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94205-6_3

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (12)

Extensional higher-order paramodulation in Leo-III ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition with lambdas ⋮ A comprehensive framework for saturation theorem proving ⋮ Superposition for full higher-order logic ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Larry Wos: visions of automated reasoning

Uses Software

• LEO-II
• Isabelle/HOL
• VAMPIRE
• SPASS
• TPTP
• Satallax
• StarExec
• E Theorem Prover
• Leo-III
• Zipperposition

This page was built for publication: Superposition for \(\lambda\)-free higher-order logic