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 semi-automatic theorem prover, just to name its most common uses.
ACL2 Version 8.3 ... paper note icon Differences from Version 8.2 tiny warning icon filing ... April 14, 2020 ... * ACL2+Books Manual (Version 8.3) ... * ACL2 User's Manual (Version 8.3)...
-
ACP is an automated confluence prover for term rewriting systems (TRSs). A distinct feature of ACP is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama,1988), layer-preserving (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 first-order logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativity-commutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete.