Superposition for lambda-free higher-order logic
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 3732007 (Why is no real title available?)
- scientific article; zbMATH DE number 67454 (Why is no real title available?)
- scientific article; zbMATH DE number 7015113 (Why is no real title available?)
- scientific article; zbMATH DE number 2090293 (Why is no real title available?)
- scientific article; zbMATH DE number 837700 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3362981 (Why is no real title available?)
- A Focused Sequent Calculus for Higher-Order Logic
- A Lambda-Free Higher-Order Recursive Path Order
- A Linear Spine Calculus
- A combinator-based superposition calculus for higher-order logic
- A compact representation of proofs
- A comprehensive framework for saturation theorem proving
- A formulation of the simple theory of types
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Automated Reasoning
- Classical type theory
- Completeness in the theory of types
- Detecting inconsistencies in large first-order knowledge bases
- Encoding monomorphic and polymorphic types
- Expressing polymorphic types in a many-sorted language
- Extensional crisis and proving identity
- Faster, higher, stronger: E 2.3
- Fingerprint indexing for paramodulation and rewriting
- Goal directed strategies for paramodulation
- Hammering towards QED
- Higher order unification via explicit substitutions
- Higher-order unification via combinators
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- LEO-II and Satallax on the Sledgehammer test bench
- Paramodulation with non-monotonic orderings and simplification
- Polynomial interpretations for higher-order rewriting
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Proving Theorems with the Modification Method
- Resolution in type theory
- Resolution theorem proving
- Restricted combinatory unification
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Satallax: An Automatic Higher-Order Prover
- Second-Order Logic and Foundations of Mathematics
- Sledgehammer: judgement day
- Superposition for -free higher-order logic
- Superposition with structural induction
- System description: E 1.8
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- The TPTP typed first-order form with arithmetic
- The higher-order prover Leo-III
- Translating higher-order clauses to first-order clauses
- Types, tableaus, and Gödel's God
- Uncurrying for termination and complexity
- Unification in a combination of arbitrary disjoint equational theories
Cited in
(11)- 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
- Hammering higher order set theory
- A modular formalization of superposition in Isabelle/HOL
- 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
Describes a project that uses
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)
