Superposition for higher-order logic
From MaRDI portal
Publication:6156638
DOI10.1007/s10817-022-09649-9OpenAlexW3199457844MaRDI QIDQ6156638
Sophie Tourret, Petar Vukmirović, Alexander Bentkamp, Jasmin Christian Blanchette
Publication date: 14 June 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09649-9
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On connections and higher-order logic
- Higher-order rewrite systems and their confluence
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Mechanizing \(\omega\)-order type theory through unification
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Types, tableaus, and Gödel's God
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The higher-order prover Leo-III
- Superposition for full higher-order logic
- A combinator-based superposition calculus for higher-order logic
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Satallax: An Automatic Higher-Order Prover
- The computability path ordering
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- A Linear Spine Calculus
- Sledgehammer: Judgement Day
- Superposition with lambdas
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
