A combinator-based superposition calculus for higher-order logic

DOI10.1007/978-3-030-51074-9_16OpenAlexW3040578348MaRDI QIDQ2096452

Ahmed Bhayat, Giles Reger

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_16

Mathematics Subject Classification ID

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

Related Items (17)

Improving automation for higher-order proof steps ⋮ A Polymorphic Vampire ⋮ Unnamed Item ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Superposition for higher-order logic ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ A comprehensive framework for saturation theorem proving ⋮ Superposition for full higher-order logic ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Lash 1.0 (system description) ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10 ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• VAMPIRE
• TPTP
• Satallax
• Sledgehammer
• StarExec
• E Theorem Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• On connections and higher-order logic
• A compact representation of proofs
• Hammer for Coq: automation for dependent type theory
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Superposition for \(\lambda\)-free higher-order logic
• The higher-order prover Leo-III
• A Knuth-Bendix-like ordering for orienting combinator equations
• Extending SMT solvers to higher-order logic
• Restricted combinatory unification
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Translating higher-order clauses to first-order clauses
• Satallax: An Automatic Higher-Order Prover
• Expressing Polymorphic Types in a Many-Sorted Language
• A Focused Sequent Calculus for Higher-Order Logic
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Superposition with lambdas

This page was built for publication: A combinator-based superposition calculus for higher-order logic