2024-11-14T19:33:54Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000169372020-10-27T05:02:43Z00934:00935:00978:00980
On Proving AC - Termination by Argument Filtering MethodOn Proving AC - Termination by Argument Filtering Methodeng通常論文http://id.nii.ac.jp/1001/00016937/Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=16937&item_no=1&attribute_id=1&file_no=1Copyright (c) 2000 by the Information Processing Society of JapanSchool of Information Science JAISTSchool of Information Science JAISTKEIICHIROU, KUSAKARIYOSHIHITO, TOYAMAThe 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）41SIG04(PRO7)65782000-06-151882-78022009-06-30