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.
- 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
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)
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.