Making higher-order superposition work
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 3907750 (Why is no real title available?)
- scientific article; zbMATH DE number 3666178 (Why is no real title available?)
- scientific article; zbMATH DE number 1324442 (Why is no real title available?)
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A combinator-based superposition calculus for higher-order logic
- A comprehensive framework for saturation theorem proving
- A unification algorithm for typed \(\bar\lambda\)-calculus
- A unifying splitting framework
- AVATAR: The Architecture for First-Order Theorem Provers
- Analytic tableaux for higher-order logic with choice
- Another algorithm for bracket abstraction
- Completely non-clausal theorem proving
- Completeness in the theory of types
- Computing small clause normal forms
- Effective normalization techniques for HOL
- Extending SMT solvers to higher-order logic
- Extensional higher-order paramodulation in Leo-III
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- Faster, higher, stronger: E 2.3
- HOL(y)Hammer: online ATP service for HOL Light
- Hammer for Coq: automation for dependent type theory
- Internal guidance for Satallax
- LEO-II and Satallax on the Sledgehammer test bench
- Layered clause selection for theory reasoning (short paper)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Making higher-order superposition work
- Mechanizing \(\omega\)-order type theory through unification
- Performance of clause selection heuristics for saturation-based theorem proving
- Playing with AVATAR
- Purely Functional Data Structures
- Reducing higher-order theorem proving to a sequence of SAT problems
- Restricted combinatory unification
- Selecting the selection
- Superposition for -free higher-order logic
- Superposition for full higher-order logic
- Superposition with equivalence reasoning and delayed clause normal form transformation.
- Superposition with first-class booleans and inprocessing clausification
- Superposition with lambdas
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- The CADE-14 ATP system competition
- The CADE-27 automated theorem proving system competition -- CASC-27
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- There is no best \(\beta \)-normalization strategy for higher-order reasoners
- Why3 -- where programs meet provers
Cited in
(10)- Superposition with lambdas
- SAT-Inspired Higher-Order Eliminations
- Superposition with structural induction
- Making higher-order superposition work
- Superposition with lambdas
- On structures of sign-boundary and diagonal vacancy-type standard contradictions
- Superposition for full higher-order logic
- Superposition for -free higher-order logic
- Term ordering diagrams
- Recurrence-Driven Summations in Automated Deduction
Describes a project that uses
Uses Software
This page was built for publication: Making higher-order superposition work
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5918575)
