The Concept of Demodulation in Theorem Proving
From MaRDI portal
Cited in
(34)- A superposition oriented theorem prover
- A structure-preserving clause form translation
- Unification theory
- Complexity and related enhancements for automated theorem-proving programs
- An implementation of hyper-resolution
- Analytic resolution in theorem proving
- Complete demodulation for automatic theorem proving
- Extension of the inverse method to axiomatic theories with equality
- Local simplification
- The kernel strategy and its use for the study of combinatory logic
- The application of automated reasoning to questions in mathematics and logic
- The problem of guaranteeing the existence of a complete set of reductions
- Horn equational theories and paramodulation
- On equational theories, unification, and (un)decidability
- The application of automated reasoning to formal models of combinatorial optimization
- Reasoning with conditional axioms
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Renamable paramodulation for automatic theorem proving with equality
- Resolution graphs
- Theorem proving with variable-constrained resolution
- The undecidability of the DA-unification problem
- Harald Ganzinger's legacy: contributions to logics and programming
- Proof normalization for resolution and paramodulation
- Local simplification
- Unification in a combination of arbitrary disjoint equational theories
- Completion of first-order clauses with equality by strict superposition
- A theorem prover for a computational logic
- On restrictions of ordered paramodulation with simplification
- The problem of demodulator adjunction
- The problem of demodulating across argument and literal boundaries
- Theorem-proving with resolution and superposition
- A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
- Steps toward a computational metaphysics
This page was built for publication: The Concept of Demodulation in Theorem Proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5538934)
