Rewrite method for theorem proving in first order theory with equality

DOI10.1016/S0747-7171(87)80024-XzbMath0637.68104MaRDI QIDQ1098649

Jieh Hsiang

Publication date: 1987

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

rewrite ruleEN-strategypredicate logic with equality

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (9)

Completion procedures as semidecision procedures ⋮ Complete equational unification based on an extension of the Knuth-Bendix completion procedure ⋮ Towards automated deduction in cP systems ⋮ Fuzzy term-rewriting system ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Discriminator varieties and symbolic computation ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ Canonical Ground Horn Theories ⋮ A categorical critical-pair completion algorithm

Cites Work

• Orderings for term-rewriting systems
• Refutational theorem proving using term-rewriting systems
• Equational methods in first order predicate calculus
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Proving Theorems with the Modification Method
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Rewrite method for theorem proving in first order theory with equality