Superposition for lambda-free higher-order logic
From MaRDI portal
Publication:4989394
Authors: Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann 
Publication date: 25 May 2021
Full work available at URL: https://arxiv.org/abs/2005.02094
Recommendations
Cites Work
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- LEO-II and Satallax on the Sledgehammer test bench
- Satallax: An Automatic Higher-Order Prover
- Title not available (Why is that?)
- Faster, higher, stronger: E 2.3
- System description: E 1.8
- Title not available (Why is that?)
- The higher-order prover Leo-III
- Isabelle/HOL. A proof assistant for higher-order logic
- Resolution theorem proving
- Uncurrying for termination and complexity
- Polynomial interpretations for higher-order rewriting
- A formulation of the simple theory of types
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Translating higher-order clauses to first-order clauses
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Sledgehammer: judgement day
- Completeness in the theory of types
- Unification in a combination of arbitrary disjoint equational theories
- A compact representation of proofs
- Resolution in type theory
- Paramodulation with non-monotonic orderings and simplification
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Types, tableaus, and Gödel's God
- Second-Order Logic and Foundations of Mathematics
- Higher-order unification via combinators
- Proving Theorems with the Modification Method
- Expressing polymorphic types in a many-sorted language
- Classical type theory
- A Linear Spine Calculus
- Title not available (Why is that?)
- Superposition with structural induction
- A combinator-based superposition calculus for higher-order logic
- Fingerprint indexing for paramodulation and rewriting
- Extensional crisis and proving identity
- Hammering towards QED
- Higher order unification via explicit substitutions
- Goal directed strategies for paramodulation
- Automated Reasoning
- A Focused Sequent Calculus for Higher-Order Logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- The TPTP typed first-order form with arithmetic
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Encoding monomorphic and polymorphic types
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Superposition for \(\lambda\)-free higher-order logic
- A comprehensive framework for saturation theorem proving
- Restricted combinatory unification
- A Lambda-Free Higher-Order Recursive Path Order
- Detecting inconsistencies in large first-order knowledge bases
- Title not available (Why is that?)
Cited In (9)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Set of support, demodulation, paramodulation: a historical perspective
- Superposition with lambdas
- Superposition for higher-order logic
- Superposition with first-class booleans and inprocessing clausification
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- A comprehensive framework for saturation theorem proving
- Superposition with Delayed Unification
- Extending a high-performance prover to higher-order logic
Uses Software
This page was built for publication: Superposition for lambda-free higher-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4989394)
