A Technique for Establishing Completeness Results in Theorem Proving with Equality

DOI10.1137/0212006MaRDI QIDQ3673152zbMATHOpenAlexFDO

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)

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

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)