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

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

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

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

03B35: Mechanization of proofs and logical operations

03B16: Higher-order logic

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

Uses Software

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