A Technique for Establishing Completeness Results in Theorem Proving with Equality

DOI10.1137/0212006MaRDI QIDQ3673152zbMATH OpenOpenAlexFDO

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

completenessfirst-order logicparamodulationresolutionsemantic treesimplificationsimplification ordering

Mathematics Subject Classification ID

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

Cited in

(34)

• A superposition oriented theorem prover
• On solving the equality problem in theories defined by Horn clauses
• Rewrite method for theorem proving in first order theory with equality
• History and basic features of the critical-pair/completion procedure
• Fuzzy term-rewriting system
• Local simplification
• Deductive and inductive synthesis of equational programs
• The problem of hyperparamodulation
• Automated deduction with associative-commutative operators
• On the termination of clause graph resolution
• On using ground joinable equations in equational theorem proving
• Theorem proving modulo
• Horn equational theories and paramodulation
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Reasoning with conditional axioms
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• An empirical analysis of modal theorem provers
• 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
• Proof normalization for resolution and paramodulation
• Goal directed strategies for paramodulation
• Local simplification
• Associative-commutative deduction with constraints
• Completion procedures as semidecision procedures
• Simultaneous paramodulation
• Positive deduction modulo regular theories
• Towards a foundation of completion procedures as semidecision procedures
• Using forcing to prove completeness of resolution and paramodulation
• Theorem-proving with resolution and superposition
• Conditional equational theories and complete sets of transformations

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)