ACP (Automated Confluence Prover)

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 several divide-and-conquer criteria such as those for commutative (Toyama,1988), layer-preserving (Ohlebusch,1994) and persistent (Aoto & Toyama, 1997) combinations. Several methods for disproving confluence are also employed. 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. ACP is participating Confluence Competition (CoCo).

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,1996)
 - Strongly weight-preserving/depth-preserving root-E-closed 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)
 - Weakly-non-overlapping non-collapsing shallow TRSs (Sakai&Ogawa,2010)
 - Reduction-preserving completion (Aoto&Toyama,2012)
 - Quasi-left-linear and parallel-closed TRSs (Suzuki&Aoto&Toyama,2013)
 - Strongly-quasi-linear and hierarchically decreasing TRSs (Aoto&Toyama&Uchida,to appear in 2014)
 - Quasi-linear and linearized-decreasing TRSs (Aoto&Toyama&Uchida,to appear in 2014)
Direct confluence disproving:
 - Disproving by direct approximations using tcap/root
 - Disproving by tree-automata (growing) approximation (Jacquemard,1996)-(Durand&Middeldorp,1997)
 - Disproving by interpretation and ordering (Aoto,2013)

Support of certificates generation
For few criteria, ACP can generate certificates in CPF format, which then can be certified by a certifier such as CeTA.
    $sml @SMLload=acp.x86-linux -d -r --enable-strongly-closed --enable-interpretation-and-order --certifiable-proofs-output=cpf.xml sample.trs

The latest version is 0.51. 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.51 2015.8.18 acp.x86-linux Linux (i386) 110.77
0.50 2014.7.2 acp.x86-linux Linux (i386) 110.76
acp.x86-darwin Mac OS X (intel) 110.76

Following bugs are identified and corrected.
 - In ver.0.40, non-confluence proof by tree-automata approximation contains a bug.
 - In ver.0.31, simple-right-linearity check was incorrect. It does not detect non-linearity if the non-linear variable have even number of occurrences in rhs of the rewrite rule. (Thanks are due to Yoshiyuki Ito (JAIST).)
 - In ver.0.31, the implementation of polynomial intepretation contains some bugs.

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.50
the main page of version 0.41
the main page of version 0.31
the main page of version 0.20
the main page of version 0.11a

Please send any requests and comments to webmaster