http://swrc.ontoware.org/ontology#Article
On Proving AC - Termination by Argument Filtering Method
en
通常論文
School of Information Science JAIST
School of Information Science JAIST
KEIICHIROU KUSAKARI
YOSHIHITO TOYAMA
The notion of dependency pairs is widely used for proving termination of TRSs. Recently this notion was extended to AC-TRSs. Using AC-dependency pairs we can easily show the AC-termination property of AC-TRSs to which traditional techniques cannot be applied. On this notion a weak AC-reduction pair plays an important role. In this paper we introduce the argument filtering method which designs a weak AC-reduction pair from an arbitrary AC-reduction order. Moreover we improve the method in two directions. One is the lexicographic argument filtering method which lexicographically combines argument filtering functions to compare AC-dependency pairs. Another one is an extension by AC-multiset extension. These methods offer useful means to prove AC-termination of complicated AC-TRSs."
The notion of dependency pairs is widely used for proving termination of TRSs. Recently, this notion was extended to AC-TRSs. Using AC-dependency pairs, we can easily show the AC-termination property of AC-TRSs to which traditional techniques cannot be applied. On this notion, a weak AC-reduction pair plays an important role. In this paper, we introduce the argument filtering method which designs a weak AC-reduction pair from an arbitrary AC-reduction order. Moreover we improve the method in two directions. One is the lexicographic argument filtering method which lexicographically combines argument filtering functions to compare AC-dependency pairs. Another one is an extension by AC-multiset extension. These methods offer useful means to prove AC-termination of complicated AC-TRSs."
AA11464814
情報処理学会論文誌プログラミング（PRO）
41
SIG04(PRO7)
65-78
2000-06-15
1882-7802