CPF-TRS Category

The CPF-TRS category deals with certified (non-)confluence proofs of first-order term rewrite systems. It is a component category of the CPF category.

Input

The competition uses the same collection of problems as those for the TRS category.

Problem

The problem is to answer a formalized (non-)confluence proof of the question whether the input TRS is confluent or not.

Problem Selection

The same collection of problems as TRS category is used.

Output Format

Tools should output certifiable proofs as well as the result of certification: YES followed by a certifiable proof (e.g. a proof in cpf format) if the confluence proof is certified, and NO followed by a certifiable proof if the non-confluence proof is certified.

Due to the fact that there is currently only one certifier, CeTA, certifiable proofs produced will be in the certifiable proof format (CPF). An example of the output can be found here.

Scoring

The scoring is same as for the TRS category.