On fairness of completion-based theorem proving strategies

DOI10.1007/3-540-53904-2_109zbMath1503.03016OpenAlexW1520405208MaRDI QIDQ5055773

Jieh Hsiang, Maria Paola Bonacina

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-53904-2_109

Mathematics Subject Classification ID

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

Related Items

Completion procedures as semidecision procedures, Relative termination via dependency pairs, On the modelling of search in theorem proving -- towards a theory of strategy analysis

Cites Work

• Orderings for term-rewriting systems
• How to avoid the derivation of redundant clauses in reasoning systems
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A maximal-literal unit strategy for horn clauses
• Completion of first-order clauses with equality by strict superposition
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item