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 is a semi-decision procedure for strong confluence and strong commutation of the multistep-rewrite relation(s) for left-linear TRSs.

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>

• MAYBE, followed by some explanation
  This indicates that either the input is not left-linear or not well-formed, or it shows which simultaneous critical pairs cannot be joined. In the latter case, the multistep rewrite relation/relations is/are not strongly confluent/commutating, provided that the unverified search algorithm has no logical error.
• 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.