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. This paper also presents a new decision procedure for word 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.

翻译：尽管关于字符串等式的推理已广泛研究数十年，但针对字符串上一般子句的等式推理研究甚少。本文提出一种新的字符串超项演算，并建立面向字符串上子句的等式定理证明框架。该框架为字符串上子句提供饱和规程，并证明所提出的含收缩规则的超项演算具有反驳完备性。此外，本文提出一种新的字符串词问题判定规程：对于字符串上条件等式集R，若R能在本文推理系统下有限饱和，则可判定该词问题。