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 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
- 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, 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.
- 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.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