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&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)
- Reduction-preserving completion (Aoto&Toyama,2012)
- Download
- The source code is available from here.
- Heap images for some platforms are also available:
- 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