この論文をさがす
説明
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."
収録刊行物
-
- 情報処理学会論文誌プログラミング（PRO）
-
情報処理学会論文誌プログラミング（PRO） 41 (SIG04(PRO7)), 65-78, 2000-06-15
情報処理学会
- Tweet
キーワード
詳細情報 詳細情報について
-
- CRID
- 1050564287845105408
-
- NII論文ID
- 110002725390
-
- NII書誌ID
- AA11464814
-
- ISSN
- 18827802
- 03875806
-
- NDL書誌ID
- 5731833
-
- 本文言語コード
- en
-
- 資料種別
- journal article
-
- データソース種別
-
- IRDB
- NDLサーチ
- CiNii Articles