  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.
