A Technique for Establishing Completeness Results in Theorem Proving with Equality

DOI10.1137/0212006zbMATH Open0522.68087OpenAlexW2051518991MaRDI QIDQ3673152FDOQ3673152

Authors: 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

resolutioncompletenessfirst-order logicsimplificationparamodulationsimplification orderingsemantic tree

Mathematics Subject Classification ID

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

Cited In (34)

• Deductive and inductive synthesis of equational programs
• 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
• A superposition oriented theorem prover
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Goal directed strategies for paramodulation
• On using ground joinable equations in equational theorem proving
• Horn equational theories and paramodulation
• On the termination of clause graph resolution
• Local simplification
• Harald Ganzinger's legacy: contributions to logics and programming
• Local simplification
• Optimized encodings of fragments of type theory in first order logic
• Towards a foundation of completion procedures as semidecision procedures
• Theorem-proving with resolution and superposition
• Proof normalization for resolution and paramodulation
• Simultaneous paramodulation
• An empirical analysis of modal theorem provers
• Reasoning with conditional axioms
• The problem of hyperparamodulation
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• From search to computation: redundancy criteria and simplification at work
• Fuzzy term-rewriting system
• Automated deduction with associative-commutative operators
• History and basic features of the critical-pair/completion procedure
• Conditional equational theories and complete sets of transformations
• Theorem proving modulo
• Completion procedures as semidecision procedures
• SPASS \& FLOTTER version 0.42
• On solving the equality problem in theories defined by Horn clauses
• Associative-commutative deduction with constraints
• Using forcing to prove completeness of resolution and paramodulation

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3673152)