ACP (Automated Confluence Prover)


Description
ACP is an automated confluence prover for term rewriting systems (TRSs). ACP integrates multiple direct criteria for guaranteeing confluence of TRSs; see below for the list of implemented criteria. It also incorporates divide 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 Linux/Unix platforms. It requires a SAT prover such as minisat and an SMT prover yices as external provers.
It might be helpful to replace the built-in (relative) termination prover with more dedicated provers such as TTT2 and AProVE.

Specifying input TRS
The input TRS is specified in a file in the (old) TPDB format. Although TPDB format allows to specify various rewriting strategies and rewriting modulo equations, proving confluence of TRSs under such varieties of rewriting is beyond the scope of the current version of ACP.
A collection of examples of TRSs extracted from the literatures on confluence can be found here.

How to use
ACP is provided as a heap image (such as acp.x86-linux) that can be loaded into SML/NJ runtime systems. The ACP heap image can be created from the source code using SML/NJ; for several platforms, it can be downloaded from the Download section below. 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 and yices are placed. To see possible options, type
   %sml @SMLload=acp.x86-linux --help

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&Oyamaguchi&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&Oyamaguchi&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)
 - Reduction-preserving completion (Aoto&Toyama,2012)

Download
The source code is available from here.
Heap images for some platforms are also available:

Version Date Heap image OS (Arch) Version of SML/NJ
0.31 2012.5.23 acp.x86-linux Linux (i386) 110.74
0.30 2012.5.16 acp.x86-darwin Mac OS X (intel) 110.74

References
Version 0.11a 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].
[1]   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.
[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.

Old pages
the main page of version 0.20
the main page of version 0.11a


Please send any requests and comments to webmaster