Equational theorem proving for clauses over strings
Dohan KimMathematical Structures in Computer Science (MSCS) 2024.
Abstract
Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a
new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition
calculus with contraction rules is refutationally complete. In particular, this paper presents a new decision procedure for solving word problems over strings and provides a new method of solving unification
problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system with contraction rules.
BibTeX
@article{DBLP:journals/mscs/Kim24,
author = {Dohan Kim},
title = {Equational theorem proving for clauses over strings},
journal = {Math. Struct. Comput. Sci.},
volume = {34},
number = {10},
pages = {1055—1078},
year = {2024},
url = {https://doi.org/10.1017/s0960129524000112},
doi = {10.1017/S0960129524000112},
timestamp = {Tue, 01 Apr 2025 19:02:42 +0200},
biburl = {https://dblp.org/rec/journals/mscs/Kim24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}