Proving Theorems with the Modification Method
From MaRDI portal
(Redirected from Publication:4099229)
Cited in
(41)- Computing finite models by reduction to function-free clause logic
- Theory decision by decomposition
- On solving the equality problem in theories defined by Horn clauses
- Rewrite method for theorem proving in first order theory with equality
- Narrowing vs. SLD-resolution
- A simplified problem reduction format
- Analytic resolution in theorem proving
- Paramodulated connection graphs
- Deductive and inductive synthesis of equational programs
- The problem of hyperparamodulation
- Automated deduction with associative-commutative operators
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- A calculus combining resolution and enumeration for building finite models
- Horn equational theories and paramodulation
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- -paramodulation method for a lattice-valued logic L_nF(X) with equality
- Kernel-LEAF: A logic plus functional language
- Craig interpolation with clausal first-order tableaux
- Subgoal alternation in model elimination
- The disconnection method
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Superposition for lambda-free higher-order logic
- Proof normalization for resolution and paramodulation
- Goal directed strategies for paramodulation
- Ordered chaining for total orderings
- Associative-commutative deduction with constraints
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- What you always wanted to know about rigid \(E\)-unification
- Conditional term rewriting and first-order theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Positive deduction modulo regular theories
- Constraint learning for non-confluent proof search
- Finding connections via satisfiability solving
- Equality and abductive residua for Horn clauses
- Using forcing to prove completeness of resolution and paramodulation
- Refutational theorem proving using term-rewriting systems
- SAD as a mathematical assistant -- how should we go from here to there?
- The disconnection tableau calculus
- Superposition-based equality handling for analytic tableaux
- Connection tableaux with lazy 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)
