CPF-TRS Category
The CPF-TRS category deals with certified (non-)confluence proofs of first-order term rewrite systems.
Format
The problem is to produce a formalized
(non-)confluence proof of the input TRS.
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 TRS category are selected.