Completion procedures as semidecision procedures

DOI10.1007/3-540-54317-1_92OpenAlexW1595261588MaRDI QIDQ5881279

Maria Paola Bonacina, Jieh Hsiang

Publication date: 9 March 2023

Published in: Conditional and Typed Rewriting Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-54317-1_92

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

A rewriting approach to satisfiability procedures. ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis

Uses Software

• SbReve2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proofs by induction in equational theories with constructors
• Refutational theorem proving using term-rewriting systems
• Automated proofs of the Moufang identities in alternative rings
• Proof by consistency
• Termination of rewriting
• Rewrite method for theorem proving in first order theory with equality
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Computing with rewrite systems
• Semantic confluence tests and completion methods
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• On fairness of completion-based theorem proving strategies