Paper Info
Title
Proving Confluence of Term Rewriting Systems Automatically
Abstract
We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide---and---conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.
Year
DOI
Venue
2009
10.1007/978-3-642-02348-4_7
RTA
Keywords
Field
DocType
distinctive feature,term rewriting systems automatically,proving confluence,direct confluence criterion,whole system,prover decomposes,technical ingredient,automated confluence prover,divide and conquer
Discrete mathematics,Commutative property,Computer science,Algorithm,Theoretical computer science,Critical pair,Confluence,Distinctive feature,Rewriting,Gas meter prover
Conference
Volume
ISSN
Citations 
5595
0302-9743
24
PageRank 
References 
Authors
1.23
19
3
Name
Order
Citations
PageRank
Takahito Aoto112117.53
Junichi Yoshida2241.23
Yoshihito Toyama353349.60