GCR Category

The GCR category deals with ground confluence of many-sorted term rewrite systems (MSTRSs).

Input

The input is a MSTRS, specified in the MSTRS format.

Problem

An MSTRS is ground confluent if confluence holds on the set of ground terms. The problem is to answer the question whether the input MSTRS is ground confluent or not.

Problem Selection

Problems are selected from those with tags either 'mstrs' and 'literature' or 'trs' and 'literature' in our problem database (Cops). The latter problems are translated to MSTRS format having a single sort, prior to giving them to GCR tools.

Only non-confluent problems are considered, where non-confluence is identified mechanically or manually. Thus, the problems are selected from those that can be proved non-confluent by some CoCo 2016 participants, Cops ♯24, ♯26, ♯47, ♯52, ♯54, ♯56, ♯57, ♯58 and ♯497. (The list may be updated by newly submitted problems.)

If the number of such problems exceeds 100, then 100 problems are selected from these problems; otherwise, all of them are considered. Our advisory board performs the selection using a random number.

Output Format

The output format should follow the same rules as for the TRS category.

Scoring

The scoring is the same as for the TRS category.