On Proving AC - Termination by Argument Filtering Method

IPSJ Web Site 17 References

Search this article

Description

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."

Journal

References(17)*help

See more

Keywords

Details 詳細情報について

Report a problem

Back to top