Superposition with lambdas
From MaRDI portal
Publication:5918381
DOI10.1007/s10817-021-09595-yOpenAlexW3194933338MaRDI QIDQ5918381
Uwe Waldmann, Petar Vukmirović, Alexander Bentkamp, Sophie Tourret, Jasmin Christian Blanchette
Publication date: 24 November 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-021-09595-y
Related Items (7)
The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Superposition for higher-order logic ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition for full higher-order logic ⋮ A comprehensive framework for saturation theorem proving ⋮ SAT-Inspired Eliminations for Superposition
Uses Software
Cites Work
- The higher-order prover \textsc{Leo}-II
- Analytic tableaux for higher-order logic with choice
- 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
- Hammer for Coq: automation for dependent type theory
- Superposition with structural induction
- 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
- Higher-order unification revisited: Complete sets of transformations
- TPS: A theorem-proving system for classical type theory
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- A combinator-based superposition calculus for higher-order logic
- Extending SMT solvers to higher-order logic
- Restricted combinatory unification
- Faster, higher, stronger: E 2.3
- Translating higher-order clauses to first-order clauses
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Satallax: An Automatic Higher-Order Prover
- Fingerprint Indexing for Paramodulation and Rewriting
- Encoding Monomorphic and Polymorphic Types
- Multimodal and intuitionistic logics in simple type theory
- A Focused Sequent Calculus for Higher-Order Logic
- The computability path ordering
- Regular Patterns in Second-Order Unification
- Extensional Crisis and Proving Identity
- Polymorphic higher-order recursive path orderings
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- A Linear Spine Calculus
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- The CADE-27 Automated theorem proving System Competition – CASC-27
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Resolution in type theory
- Sledgehammer: Judgement Day
- Completeness in the theory of types
- A comprehensive framework for saturation theorem proving
- Superposition with lambdas
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Superposition with lambdas
