Termination Property of Inverse Finite Path Overlapping Term Rewriting System is Decidable

Toshinori TAKAI  Yuichi KAJI  Hiroyuki SEKI  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E85-D   No.3   pp.487-496
Publication Date: 2002/03/01
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Theory/Models of Computation
Keyword: 
term rewriting system,  termination,  tree automaton,  

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



Summary: 
We propose a new decidable subclass of term rewriting systems (TRSs) for which strongly normalizing (SN) property is decidable. The new class is called almost orthogonal inverse finite path overlapping TRSs (AO-FPO-1-TRSs) and the class properly includes AO growing TRSs for which SN is decidable. Tree automata technique is used to show that SN is decidable for AO-FPO-1-TRSs.