ACP (Automated Confluence Prover)


Description
ACP is an automated confluence prover for term rewriting systems (TRSs). A distinct feature of ACP 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.

What is needed to run the ACP?
ACP is written in Standard ML of New Jersey (SML/NJ). To run the ACP, you need Standard ML of New Jersey. We are expecting only Unix platforms. Furthermore, if you use an internal termination prover then a SAT solver minisat is needed. Alternatively, you can use external termination provers such as TTT2 and AProVE.

How to use
ACP is provided as a heap image (such as acp.x86-linux) that can be loaded into SML/NJ runtime systems. To download the images, jump to the Download section below. The input TRS is specified in a file in the TPDB format. Basically, you can run the ACP by the command
   %sml @SMLload=acp.x86-linux filename
on a directory where the heap image acp.x86-linux and the minisat are placed. To see possible options, type
   %sml @SMLload=acp.x86-linux --help

Experiments
We have prepared a collection of 103 examples extracted from the literatures on confluence (crexamples-090206.tgz). We have tested confluence proving using various combinations of decomposition techniques. All tests have been performed in a PC equipped with Intel Xeon processors of 2.66GHz and a memory of 7GB. The table below summarizes our experimental results. d, p, l, c, c' stand for direct methods, (minimal) persistent decomposition, (mimimal) layer-preserving decomposition, minimal commutative decomposition, and (possibly non-minimal) commutative decomposition, respectively. Details of the experiment can be found here.

d dp dl dc dc' dpl dpc dpc' dlc dlc' dplc dplc'
success (CR) 30 35 34 41 43 37 47 49 46 47 49 50
success (NON-CR) 13 13 13 13 13 13 13 13 13 13 13 13
failure 60 55 56 49 47 53 43 41 44 43 41 40
timeout (60 sec.) 0 0 0 0 0 0 0 0 0 0 0 0
total time (sec.) 4.1 4.4 4.8 7.0 33.6 4.9 8.1 30.9 7.6 34.2 8.1 34.4

Download
The latest version is 0.11a, which is described in the paper [1]. It is a slightly updated version of version 0.10, which was used in the submitted version of [1]. Older versions which we aren't putting on the web have been described also in [2,3].

Version Date Heap image OS (Arch) Version of SML/NJ
0.11a 2009.4.13 acp.x86-linux Linux (i386) 110.69
0.10 2009.2.6 acp.x86-linux Linux (i386) 110.69
acp.x86-darwin Mac OS X (intel) 110.69
acp.ppc-darwin Mac OS X (ppc) 110.69
acp.x86-linux Linux (i386) 110.0.7

References
[1]   Takahito Aoto, Junichi Yoshida, Yoshihito Toyama, Proving confluence of term rewriting systems automatically, In Proc. of RTA 2009, to appear.
[2]   Junichi Yoshida, Takahito Aoto, Yoshihito Toyama, Automating confluence check of term rewriting systems (in Japanese), Computer Software, Vol.26, No.2, pp.76-92, 2009.
[3]   Junichi Yoshida, Takahito Aoto and Yoshihito Toyama, Automating confluence check of term rewriting systems (in Japanese), In Proceedings of the Forum on Information Technology 2007 (FIT2007), Information Technology Letters, Vol.6, pp.31-34, 2007.


Please send any requests and comments to webmaster