Making higher-order superposition work
From MaRDI portal
Publication:5918575
DOI10.1007/s10817-021-09613-zOpenAlexW4206463158MaRDI QIDQ5918575
Petar Vukmirović, Sophie Tourret, Visa Nummelin, Jasmin Christian Blanchette, Simon Cruanes, Alexander Bentkamp
Publication date: 12 December 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-021-09613-z
Related Items
Uses Software
Cites Work
- Unnamed Item
- 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 \(\bar\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
- LEO-II and Satallax on the Sledgehammer test bench
- HOL(y)Hammer: online ATP service for HOL Light
- A unifying splitting framework
- Superposition with first-class booleans and inprocessing clausification
- 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
- Extensional higher-order paramodulation in Leo-III
- 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 10th IJCAR automated theorem proving system competition – CASC-J10
- The CADE-27 Automated theorem proving System Competition – CASC-27
- Why3 — Where Programs Meet Provers
- Logic for Programming, Artificial Intelligence, and Reasoning
- Completeness in the theory of types
- Automated Deduction – CADE-19
- Superposition with lambdas
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
