Path Rewriting and Combined Word Problems
Camillo Fiorentini, Silvio Ghilardi · 2003
. We give an algorithm solving combined word problems (over non necessarily disjoint signatures) based on rewriting of equivalence classes of terms. The canonical rewriting system we introduce consists of few transparent rules and is obtained by applying Knuth-Bendix completion procedure to presentations of pushouts among categories with products. It applies to pairs of theories which are both constructible over their common reduct (on which we do not make any special assumption) . Lavoro svolto nell'ambito del progetto MURST \\Logica". 1 1 Introduction An essential problem in automated deduction consists in integrating theorem provers which are able to perform separated tasks. In the eld of equational logic, this leads in particular to the following question: suppose you are able to solve word problems for theories T 1 ; T 2 ; can you solve word problem for T 1 [ T 2 ? Better, can you design an algorithm taking as input two arbitrary algorithms for word problems for T 1 and T 2...