A combinator-based superposition calculus for higher-order logic
From MaRDI portal
Publication:2096452
DOI10.1007/978-3-030-51074-9_16OpenAlexW3040578348MaRDI QIDQ2096452
Publication date: 9 November 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_16
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
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