Proving Theorems with the Modification Method
From MaRDI portal
Publication:4099229
Cited in
(39)- Associative-commutative deduction with constraints
- Using forcing to prove completeness of resolution and paramodulation
- Deductive and inductive synthesis of equational programs
- Equality and abductive residua for Horn clauses
- Rewrite method for theorem proving in first order theory with equality
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Positive deduction modulo regular theories
- Paramodulated connection graphs
- Goal directed strategies for paramodulation
- The disconnection method
- Horn equational theories and paramodulation
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Refutational theorem proving using term-rewriting systems
- Ordered chaining for total orderings
- Conditional term rewriting and first-order theorem proving
- What you always wanted to know about rigid \(E\)-unification
- Computing finite models by reduction to function-free clause logic
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- A calculus combining resolution and enumeration for building finite models
- Superposition-based equality handling for analytic tableaux
- The disconnection tableau calculus
- Theory decision by decomposition
- Proof normalization for resolution and paramodulation
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
- Narrowing vs. SLD-resolution
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Craig interpolation with clausal first-order tableaux
- A simplified problem reduction format
- The problem of hyperparamodulation
- SAD as a mathematical assistant -- how should we go from here to there?
- Automated deduction with associative-commutative operators
- Subgoal alternation in model elimination
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Connection tableaux with lazy paramodulation
- Kernel-LEAF: A logic plus functional language
- On solving the equality problem in theories defined by Horn clauses
- Analytic resolution in theorem proving
This page was built for publication: Proving Theorems with the Modification Method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4099229)
