The HRS category deals with confluence of higher-order rewrite systems (HRSs) described in
- R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, 1998.
The input is a higher-order rewrite system (new!), specified in the HRS format.
An HRS is confluent if any two convertible terms are joinable modulo beta-eta-equivalence. The problem is to answer the question whether the input HRS is confluent or not confluent.
Problems with tags 'hrs' and 'literature' in our problem database (Cops) are used. 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.
The output format should follow the same rule as that of the TRS category.
The scoring is same as the TRS category.