scientific article; zbMATH DE number 7350767
From MaRDI portal
Publication:4989394
Alexander Bentkamp, Uwe Waldmann, Simon Cruanes, Jasmin Christian Blanchette
Publication date: 25 May 2021
Full work available at URL: https://arxiv.org/abs/2005.02094
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (6)
The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Superposition for higher-order logic ⋮ Superposition with lambdas ⋮ A comprehensive framework for saturation theorem proving ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Uncurrying for termination and complexity
- Paramodulation with non-monotonic orderings and simplification
- Unification in a combination of arbitrary disjoint equational theories
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A compact representation of proofs
- Types, tableaus, and Gödel's God
- Isabelle/HOL. A proof assistant for higher-order logic
- Superposition with structural induction
- Superposition for \(\lambda\)-free higher-order logic
- The higher-order prover Leo-III
- Higher order unification via explicit substitutions
- LEO-II and Satallax on the Sledgehammer test bench
- A combinator-based superposition calculus for higher-order logic
- Restricted combinatory unification
- Faster, higher, stronger: E 2.3
- Higher-order unification via combinators
- Detecting inconsistencies in large first-order knowledge bases
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Translating higher-order clauses to first-order clauses
- System Description: E 1.8
- The TPTP Typed First-Order Form with Arithmetic
- Satallax: An Automatic Higher-Order Prover
- Fingerprint Indexing for Paramodulation and Rewriting
- Encoding Monomorphic and Polymorphic Types
- A Lambda-Free Higher-Order Recursive Path Order
- Expressing Polymorphic Types in a Many-Sorted Language
- A Focused Sequent Calculus for Higher-Order Logic
- Extensional Crisis and Proving Identity
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Proving Theorems with the Modification Method
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Second-Order Logic and Foundations of Mathematics
- A Linear Spine Calculus
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Goal directed strategies for paramodulation
- Polynomial Interpretations for Higher-Order Rewriting
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Hammering towards QED
- Automated Reasoning
- Resolution in type theory
- Sledgehammer: Judgement Day
- A formulation of the simple theory of types
- Completeness in the theory of types
- A comprehensive framework for saturation theorem proving
This page was built for publication:
