Proving Theorems with the Modification Method

Cited In (39)

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
Title not available (Why is that?)
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}
Proof normalization for resolution and paramodulation
A calculus combining resolution and enumeration for building finite models
Theory decision by decomposition
Superposition-based equality handling for analytic tableaux
The disconnection tableau calculus
\( \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
Associative-commutative deduction with constraints
Analytic resolution in theorem proving
Using forcing to prove completeness of resolution and paramodulation

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)