Making higher-order superposition work
From MaRDI portal
Publication:5918403
DOI10.1007/978-3-030-79876-5_24OpenAlexW3167807588MaRDI QIDQ5918403
Visa Nummelin, Simon Cruanes, Petar Vukmirović, Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret
Publication date: 1 December 2021
Published in: Automated Deduction – CADE 28 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_24
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (9)
AC simplifications and closure redundancies in the superposition calculus ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Superposition for higher-order logic ⋮ Making higher-order superposition work ⋮ Superposition for full higher-order logic ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Lash 1.0 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Analytic tableaux for higher-order logic with choice
- Completely non-clausal theorem proving
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Mechanizing \(\omega\)-order type theory through unification
- The CADE-14 ATP system competition
- 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
- LEO-II and Satallax on the Sledgehammer test bench
- HOL(y)Hammer: online ATP service for HOL Light
- A unifying splitting framework
- Superposition for full higher-order logic
- A combinator-based superposition calculus for higher-order logic
- Layered clause selection for theory reasoning (short paper)
- Extending SMT solvers to higher-order logic
- Restricted combinatory unification
- Faster, higher, stronger: E 2.3
- Reducing higher-order theorem proving to a sequence of SAT problems
- Selecting the Selection
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- Internal Guidance for Satallax
- Effective Normalization Techniques for HOL
- AVATAR: The Architecture for First-Order Theorem Provers
- Playing with AVATAR
- There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners
- Another algorithm for bracket abstraction
- Purely Functional Data Structures
- The CADE-27 Automated theorem proving System Competition – CASC-27
- Why3 — Where Programs Meet Provers
- Logic for Programming, Artificial Intelligence, and Reasoning
- Automated Deduction – CADE-19
- Superposition with lambdas
This page was built for publication: Making higher-order superposition work
