Tools on Rewriting

ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semiautomatic theorem prover, just to name its most common uses.
[door02.gif] Start Here: Applications, Talks, Tours, and Tutorials/Demos [teacher2.gif] ACL2 Workshops, UT Seminar, and Course Materials...

ACP is an automated confluence prover for term rewriting systems (TRSs). A distinct feature of ACP is incorporation of several divideandconquer criteria such as those for commutative (Toyama,1988), layerpreserving (Ohlebusch,1994) and persistent (Aoto and 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.
the whole system. ACP is participating Confluence Competition (CoCo). ... Support of certificates generation For few criteria, ACP can generate certificates in CPF format, w...

The aim of the system daTac is to do automated deduction in firstorder logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativitycommutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete.