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).
Combining word problems through rewriting in categories with products / C. Fiorentini, S. Ghilardi. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 294:1-2(2003), pp. 103-149. [10.1016/S0304-3975(01)00248-1]
Combining word problems through rewriting in categories with products
C. FiorentiniPrimo
;S. GhilardiUltimo
2003
Abstract
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).
| File | Dimensione | Formato | |
|---|---|---|---|
|
2003_tcs.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
412.9 kB
Formato
Adobe PDF
|
412.9 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
