Approximating Dependency Graphs Using Tree Automata Techniques
Approximating Dependency Graphs Using Tree Automata Techniques
复制标题
使用树自动机技术近似依赖图
DOI：
10.1007/3-540-45744-5_49
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
A. Middeldorp
中科院分区：
文献类型：
--
作者：
A. Middeldorp
Arts和Giesl的依赖对方法是自动证明术语重写系统可终止性的最有效的技术。我们表明，该方法可以通过使用树自动机技术，以获得更好的依赖图的近似。该图确定了为了得出终止结论而需要解决的排序约束。我们进一步表明，通过使用我们的近似的依赖对方法提供了一个决策程序终止右地面重写系统。
The dependency pair method of Arts and Giesl is the most powerful technique for proving termination of term rewrite systems automatically. We show that the method can be improved by using tree automata techniques to obtain better approximations of the dependency graph. This graph determines the ordering constraints that need to be solved in order to conclude termination. We further show that by using our approximations the dependency pair method provides a decision procedure for termination of right-ground rewrite systems.
左线性增长术语重写系统的可判定性
DOI：
--
发表时间：
2002
期刊：
Information and Computation 178
影响因子：
--
作者：
K.Kageyama;S.Kadowaki;Takahito Nagaya
通讯作者：
Takahito Nagaya