CeTA-Prover

CeTA-Prover is an automated prover for confluence and commutation. It expects ARI-files as input. Its output are CPF3 certificates that can be checked by CeTA.

CeTA-Prover was developed using verified functional programs from IsaFoR/CeTA in combination with further unverified Haskell code.

In its initial version 1.0, CeTA-Prover contains a semi-decision procedure for strong confluence and strong commutation of the multistep-rewrite relation(s) for left-linear TRSs. Moreover, if further contains a semi-decision procedure for Toyama's confluence and commutation criterion via parallel critical pairs.

CeTA-Prover is also used as a library within the nonreach infeasibility and feasibility prover. Here, CeTA-Prover converts the minimalistic feasibility proofs of an internal search algorithm in nonreach into more detailed once where rewrite sequences are reconstructed; these detailed proofs are then further exported to human readable form or to CPF3.

Installation instructions

• Install ghc and cabal.
• Download and extract the source code of CeTA-Prover.
• Build and install CeTA-Prover:

  cabal install exe:ceta-prover

• Run CeTA-Prover on .ari-files:

  ceta-prover <filename.ari>

• Run CeTA-Prover without arguments to see command-line options, e.g., for only selecting Okui's criterion or only Toyama's.

• MAYBE, followed by some explanation
  This indicates that either the input is not left-linear or not well-formed, or it shows which critical pairs cannot be joined. In the latter case, the criteria of Okui and Toyama are not applicable, provided that the unverified search algorithm has no logical error. In case of Okui's criterion this also means that the multistep rewrite relation (or relations) are not strongly confluence (or commuting).
• YES, followed by a CPF3 proof
  The proof can be checked by CeTA.
• NON-TERMINATION
  Since CeTA-Prover performs an unbounded breadth-first search, it can happen that CeTA-Prover just does not terminate.