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 several divideandconquer criteria such as
those for commutative (Toyama,1988), layerpreserving (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 builtin (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.x86linux)
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.x86linux filename
on a directory where the heap image acp.x86linux and
the minisat and yices are placed.
To see possible options, type
%sml @SMLload=acp.x86linux help
 Implemented criteria

Currently the following criteria are supported (for some critera, approximations are employed).
Divideandconquer criteria:
 commutative decomposition (Toyama,1988)
 layerpreserving decomposition (Ohlebusch,1994)
 persistent decomposition (Toyama,1987)(Aoto&Toyama,1997)
Direct confluence criteria:
 KnuthBendix criterion (Knuth&Bendix,1970)
 Linear strongly closed TRSs (Huet,1980)
 Criterion based on parallel critical pairs (Toyama,1981)
 Simplerightlinear nonEoverlapping TRSs (Ohta&Oyamaguchi&Toyama,1995)
 Leftlinear development closed TRSs (Huet,1980)(Toyama,1988)(van Oostrom,1997)
 Criterion based on simultaneous critical pairs (Okui,1998)
 Strongly depthpreserving nonEoverlapping TRSs (Gomi&Oyamaguchi&Ohta,1996)
 Strongly weightpreserving/depthpreserving rootEclosed TRSs (Gomi&Oyamaguchi&Ohta,1998)
 Leftlinear upsideparallelclosed or outsideclosed TRSs (Oyamaguchi&Ohta,2004)
 Decreasing diagrams based on rulelabelling (van Oostrom,2008)(Aoto,2010)
 Weaklynonoverlapping noncollapsing shallow TRSs (Sakai&Ogawa,2010)
 Reductionpreserving completion (Aoto&Toyama,2012)
 Quasileftlinear and parallelclosed TRSs (Suzuki&Aoto&Toyama,2013)
 Stronglyquasilinear and hierarchically decreasing TRSs (Aoto&Toyama&Uchida,to appear in 2014)
 Quasilinear and linearizeddecreasing TRSs (Aoto&Toyama&Uchida,to appear in 2014)
Direct confluence disproving:
 Disproving by direct approximations using tcap/root
 Disproving by treeautomata (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.x86linux d r
enablestronglyclosed
enableinterpretationandorder
certifiableproofsoutput=cpf.xml sample.trs
 Download
 The latest version is 0.51. The source code is available from here.
 Heap images for some platforms are also available:
 Bugs

Following bugs are identified and corrected.
 In ver.0.40, nonconfluence proof by treeautomata approximation
contains a bug.
 In ver.0.31, simplerightlinearity check was incorrect.
It does not detect nonlinearity if the nonlinear 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.
 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.93102, 2009.
 [2]
Junichi Yoshida, Takahito Aoto, Yoshihito Toyama,
Automating confluence check of term rewriting systems (in Japanese),
Computer Software, Vol.26, No.2, pp.7692, 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.3134, 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