Reducibility constraints in superposition
From MaRDI portal
Cites work
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 50648 (Why is no real title available?)
- scientific article; zbMATH DE number 1348470 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 1754649 (Why is no real title available?)
- A comprehensive framework for saturation theorem proving
- AVATAR: The Architecture for First-Order Theorem Provers
- Automated Reasoning
- Basic narrowing revisited
- Consider only general superpositions in completion procedures
- Critical pair criteria for completion
- Faster, higher, stronger: E 2.3
- Ground joinability and connectedness in the superposition calculus
- On using ground joinable equations in equational theorem proving
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Paramodulation-based theorem proving
- Proving termination with multiset orderings
- Reducibility constraints in superposition
- Redundancy criteria for constrained completion
- Resolution theorem proving
- SOLVING SYMBOLIC ORDERING CONSTRAINTS
- Solution of the Robbins problem
- Subsumption demodulation in first-order theorem proving
- Superposition with Delayed Unification
- Term Rewriting and All That
- The logic languages of the TPTP world
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Unnecessary inferences in associative-commutative completion procedures
This page was built for publication: Reducibility constraints in superposition
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034873)
