Categories

Types of Categories

Categories are divided into competition categories and demonstration categories. The former categories are intended to be persistent, whereas the latter categories are intended to be one-time events. However, categories with only one participating tool are also run as demonstration categories.

Competition Categories

In competition categories, problems are selected from our problem database (Cops). The following categories are prepared to be run as competition categories:

• TRS: confluence of first-order term rewrite systems
• CTRS: confluence of conditional term rewrite systems
• CPF: combined category of CPF-TRS and CPF-CTRS
• CPF-TRS: certified confluence of first-order term rewrite systems
• CPF-CTRS: certified confluence of conditional term rewrite systems
• HRS: confluence of higher-order rewrite systems
• GCR: ground confluence of first-order term rewrite systems
• UN: combined category of UNC, NFP and UNR
• UNC: unique normal form with respect to conversion of first-order term rewrite systems
• UNR: unique normal form with respect to reduction of first-order term rewrite systems
• NFP: normal form property of first-order term rewrite systems

In a combined category, participating tools are run on each component category separately but total scores are also computed. Participating tools may have different configurations for each component category.

Demonstration Categories

Demonstration categories are one-time events for demonstrating new attempts and/or merit of your tools. Tool authors also need to provide the problems for the competitions. For instance, the next categories are in the scope of demonstration: categories of right-ground TRSs, CTRSs of specific condition type and eTRSs, the category with 1 second time limit and the category running on large problems.

Request of New Categories

Request for new categories is via the contact email address. Please send us the following information:

• category type (competition category or demonstration category)
• description of problems and semantics (rewrite steps, confluence, etc.) together with adequate references
• a proposal of the input format (if necessary)

It is preferable that a prototype of the tool and sample problems are available at the time of the request.

For the competition categories, we presume integration of problem collections into our problems database (Cops). Thus, it is preferable to have a demonstration category, prior to requesting the category as a competition category.