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.
Depending the criteria you use, you need other softwares. If you use Knuth-Bendix criteria then then a SAT solver minisat or an external termination prover such as TTT2 and AProVE is needed. If you use decreasing diagrams technique (based on rule-labelling) then a SMT solver yices is needed.

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

Collection of examples
We have prepared a collection of examples of TRSs extracted from the literatures on confluence.
    crexamples-100410.tgz (contains 106 examples, latest version)
    crexamples-090206.tgz (contains 103 examples, obsolete)

Experiments
Details of the experiments reported in the paper [1] are found here. Those reported in the paper [2] are found here.

Implemented criteria
Currently the following criteria are supported (for some critera, approximations are employed).
Divide-and-conquer criteria:
 - commutative decomposition (Toyama,1988)
 - layer-preserving decomposition (Ohlebusch,1994)
 - persistent decomposition (Toyama,1987)-(Aoto&Toyama,1997)
Direct confluence criteria:
 - Knuth-Bendix criterion (Knuth&Bendix,1970)
 - Linear strongly closed TRSs (Huet,1980)
 - Criterion based on parallel critical pairs (Toyama,1981)
 - Simple-right-linear non-E-overlapping TRSs (Ohta&Oyamaguch&Toyama,1995)
 - Left-linear development closed TRSs (Huet,1980)-(Toyama,1988)-(van Oostrom,1997)
 - Criterion based on simultaneous critical pairs (Okui,1998)
 - Strongly depth-preserving non-E-overlapping TRSs (Gomi&Oyamaguch&Ohta,1998)
 - Left-linear upside-parallel-closed or outside-closed TRSs (Oyamaguchi&Ohta,2004)
 - Decreasing diagrams based on rule-labelling (van Oostrom,2008)-(Aoto,2010)

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

Version Date Heap image OS (Arch) Version of SML/NJ
0.20 2010.4.10 acp.x86-linux Linux (i386) 110.72
acp.x86-darwin Mac OS X (intel) 110.72
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, Automated confluence proof by decreasing diagrams based on rule-labelling, In Proc. of RTA 2010, to appear.
[2]   Takahito Aoto, Junichi Yoshida, Yoshihito Toyama, Proving confluence of term rewriting systems automatically, In Proc. of RTA 2009, LNCS, Vol.5595, pp.93-102, 2009.
[3]   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.
[4]   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.

Old pages
You can find some old pages here: the main page of version 0.11a


Please send any requests and comments to webmaster