Equational Theorem Proving for Clauses over Strings

DOI10.4204/eptcs.376.6arXiv2303.13257OpenAlexW4353057074WikidataQ121863166 ScholiaQ121863166MaRDI QIDQ6118747

Dohan Kim

Publication date: 28 February 2024

Published in: Electronic Proceedings in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2303.13257

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An efficient SMT solver for string constraints
• Testing for the Church-Rosser property
• A rewriting approach to satisfiability procedures.
• A completion procedure for finitely presented groups that is based on word cycles
• Equational theorem proving modulo
• The Knuth-Bendix Completion Procedure and Thue Systems
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• ON PRESENTATIONS OF COMMUTATIVE MONOIDS
• Cross-sections for finitely presented monoids with decidable word problems
• Unification and matching modulo nilpotence
• Term Rewriting and All That
• Conditional semi-Thue systems for presenting monoids