Termination of the Direct Sum of Rpo-Terminating Term Rewriting Systems

Masahito KURIHARA  Ikuo KAJI  

IEICE TRANSACTIONS (1976-1990)   Vol.E71   No.10   pp.975-977
Publication Date: 1988/10/25
Online ISSN: 
Print ISSN: 0000-0000
Type of Manuscript: LETTER
Category: Automaton, Language and Theory of Computing

Full Text: PDF(192.1KB)>>
Buy this Article

A term rewriting system is said to be rpoterminating if it's termination is proved with the recursive path ordering method. The direct sum R1M2 of term rewriting systems R1 and R2 is rpo-terminating iff both R1 and R2 are so.