Proving Theorems with the Modification Method
From MaRDI portal
Publication:4099229
DOI10.1137/0204036zbMath0333.68059OpenAlexW1966048066MaRDI QIDQ4099229
Publication date: 1975
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/0204036
Related Items
Conditional term rewriting and first-order theorem proving, On solving the equality problem in theories defined by Horn clauses, 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, Proof normalization for resolution and paramodulation, Goal directed strategies for paramodulation, Rewrite method for theorem proving in first order theory with equality, Kernel-LEAF: A logic plus functional language, KoMeT, Narrowing vs. SLD-resolution, \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, SAD as a mathematical assistant -- how should we go from here to there?, The disconnection tableau calculus, Superposition-based equality handling for analytic tableaux, Craig interpolation with clausal first-order tableaux, Unnamed Item, A calculus combining resolution and enumeration for building finite models, Subgoal alternation in model elimination, A simplified problem reduction format, Connection tableaux with lazy paramodulation, The disconnection method, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Equality and abductive residua for Horn clauses, Analytic resolution in theorem proving, Formalizing Bachmair and Ganzinger's ordered resolution prover, Computing finite models by reduction to function-free clause logic, Ordered chaining for total orderings, Associative-commutative deduction with constraints, Paramodulated connection graphs, Using forcing to prove completeness of resolution and paramodulation, Horn equational theories and paramodulation, What you always wanted to know about rigid E-unification, Theory decision by decomposition, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, Refutational theorem proving using term-rewriting systems, Deductive and inductive synthesis of equational programs
