CPF-CTRS Category

The CPF-CTRS category deals with certified (non-)confluence proofs of conditional term rewrite systems.

Format

The problem is to produce a formalized (non-)confluence proof of the input CTRS. Tools should output certifiable proofs as well as the result of certification: YES followed by a certifiable proof if the confluence proof is certified, and NO followed by a certifiable proof if the non-confluence proof is certified.

As there is currently only one certifier, CeTA, certifiable proofs must be in the certifiable proof format (CPF). An example of the output can be found here.

Problem Selection

The same problems as in the CTRS category are selected.