A Technique for Establishing Completeness Results in Theorem Proving with Equality

DOI10.1137/0212006zbMath0522.68087OpenAlexW2051518991MaRDI QIDQ3673152

Gerald E. Peterson

Publication date: 1983

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/ba0721cdfb68c57301abcfe9f51ffe841cd3684c

zbMATH Keywords

completenessfirst-order logicresolutionsimplificationparamodulationsimplification orderingsemantic tree

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items (32)

Completion procedures as semidecision procedures ⋮ On solving the equality problem in theories defined by Horn clauses ⋮ The problem of hyperparamodulation ⋮ Automated deduction with associative-commutative operators ⋮ On the termination of clause graph resolution ⋮ Proof normalization for resolution and paramodulation ⋮ Goal directed strategies for paramodulation ⋮ Rewrite method for theorem proving in first order theory with equality ⋮ History and basic features of the critical-pair/completion procedure ⋮ Reasoning with conditional axioms ⋮ On using ground joinable equations in equational theorem proving ⋮ Conditional equational theories and complete sets of transformations ⋮ Theorem proving modulo ⋮ Fuzzy term-rewriting system ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ SPASS & FLOTTER version 0.42 ⋮ Optimized encodings of fragments of type theory in first order logic ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Associative-commutative deduction with constraints ⋮ An empirical analysis of modal theorem provers ⋮ Local simplification ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ Theorem-proving with resolution and superposition ⋮ Local simplification ⋮ Horn equational theories and paramodulation ⋮ A superposition oriented theorem prover ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II ⋮ Deductive and inductive synthesis of equational programs

This page was built for publication: A Technique for Establishing Completeness Results in Theorem Proving with Equality