The Concept of Demodulation in Theorem Proving
From MaRDI portal
Publication:5538934
DOI10.1145/321420.321429zbMath0157.02501OpenAlexW2058514808WikidataQ114255235 ScholiaQ114255235MaRDI QIDQ5538934
No author found.
Publication date: 1967
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321420.321429
Related Items
Completion of first-order clauses with equality by strict superposition ⋮ Proof normalization for resolution and paramodulation ⋮ A structure-preserving clause form translation ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ The undecidability of the DA-unification problem ⋮ Steps toward a computational metaphysics ⋮ Unification theory ⋮ Reasoning with conditional axioms ⋮ The problem of demodulator adjunction ⋮ The problem of demodulating across argument and literal boundaries ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Complexity and related enhancements for automated theorem-proving programs ⋮ An implementation of hyper-resolution ⋮ Analytic resolution in theorem proving ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Complete demodulation for automatic theorem proving ⋮ Extension of the inverse method to axiomatic theories with equality ⋮ Local simplification ⋮ Theorem-proving with resolution and superposition ⋮ Renamable paramodulation for automatic theorem proving with equality ⋮ Resolution graphs ⋮ A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains ⋮ Local simplification ⋮ The problem of guaranteeing the existence of a complete set of reductions ⋮ Horn equational theories and paramodulation ⋮ On equational theories, unification, and (un)decidability ⋮ Theorem proving with variable-constrained resolution ⋮ The application of automated reasoning to formal models of combinatorial optimization ⋮ A superposition oriented theorem prover ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ The kernel strategy and its use for the study of combinatory logic
