Superposition with lambdas
From MaRDI portal
Recommendations
Cites work
- A combinator-based superposition calculus for higher-order logic
- A comprehensive framework for saturation theorem proving
- A Focused Sequent Calculus for Higher-Order Logic
- A Linear Spine Calculus
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Analytic tableaux for higher-order logic with choice
- ATP and presentation service for Mizar formalizations
- Classical type theory
- Completeness in the theory of types
- Encoding monomorphic and polymorphic types
- Extending SMT solvers to higher-order logic
- Extensional crisis and proving identity
- Faster, higher, stronger: E 2.3
- Fingerprint indexing for paramodulation and rewriting
- Hammer for Coq: automation for dependent type theory
- Higher order E-unification
- Higher-order rewrite systems and their confluence
- Higher-order unification and matching
- Higher-order unification revisited: Complete sets of transformations
- HOL(y)Hammer: online ATP service for HOL Light
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1301855 (Why is no real title available?)
- scientific article; zbMATH DE number 1303338 (Why is no real title available?)
- scientific article; zbMATH DE number 1341621 (Why is no real title available?)
- scientific article; zbMATH DE number 7015113 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3362981 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- Mechanizing \(\omega\)-order type theory through unification
- Multimodal and intuitionistic logics in simple type theory
- On connections and higher-order logic
- Polymorphic higher-order recursive path orderings
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Regular patterns in second-order unification
- Resolution in type theory
- Resolution theorem proving
- Restricted combinatory unification
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Satallax: An Automatic Higher-Order Prover
- Sledgehammer: judgement day
- Superposition for -free higher-order logic
- Superposition for lambda-free higher-order logic
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Superposition with lambdas
- Superposition with structural induction
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- The CADE-27 automated theorem proving system competition -- CASC-27
- The computability path ordering
- The higher-order prover \textsc{Leo}-II
- The higher-order prover Leo-III
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- TPS: A theorem-proving system for classical type theory
- Translating higher-order clauses to first-order clauses
- Types, tableaus, and Gödel's God
Cited in
(12)- Superposition for full higher-order logic
- SAT-Inspired Eliminations for Superposition
- Making higher-order superposition work
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- The 11th IJCAR automated theorem proving system competition – CASC-J11
- Superposition for higher-order logic
- Extending a high-performance prover to higher-order logic
- A modular formalization of superposition in Isabelle/HOL
- Duper: a proof-producing superposition theorem prover for dependent type theory
- Refining unification with abstraction
- Automation of Boolos' Curious Inference in Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: Superposition with lambdas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5918381)
