Superposition with Delayed Unification
From MaRDI portal
Superposition with Delayed Unification
Cites work
- A combinator-based superposition calculus for higher-order logic
- A comprehensive framework for saturation theorem proving
- A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
- A unification algorithm for typed -calculus
- AVATAR: The Architecture for First-Order Theorem Provers
- Fingerprint indexing for paramodulation and rewriting
- Goal directed strategies for paramodulation
- Higher-order unification revisited: Complete sets of transformations
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1303344 (Why is no real title available?)
- scientific article; zbMATH DE number 1348470 (Why is no real title available?)
- On restrictions of ordered paramodulation with simplification
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Superposition for lambda-free higher-order logic
- Superposition with lambdas
- The higher-order prover \textsc{Leo}-II
- The higher-order prover Leo-III
- The state of CASC
- Unification theory
- Unification with abstraction and theory instantiation in saturation-based reasoning
Cited in
(4)
This page was built for publication: Superposition with Delayed Unification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492727)