* Category type demonstration category for CoCo 2016 * Problem and Semantics Our problem is to check ground confluence of many-sorted TRSs. A many-sorted TRS R is ground confluent if R is confluent on the set of ground terms. For many-sorted TRSs, we refer e.g. Section 6.5.6 of the book: Terese, Term Rewriting Systems, Cambridge University Press, 2003. * Input and Input format The input of the problem is a many-sorted TRS. To declare many-sorted TRSs, we add the following changes to the specification of first-order TRSs (in old TPDB format): (i) Add sorted function declaration. Thus, decl is replaced as follows: ........... decl ::= VAR varlist | RULES listofrules | FUN funlist | id anylist varlist ::= | id varlist funlist ::= | fun funlist fun ::= id : sort sort ::= id | idlist -> id idlist ::= id | id , idlist ........... Furthermore, id should not contain ':'. * Example (FUN b: 0 c: 1 f: 0 -> 0 g: 0 -> 1 h: 1, 1 -> 2 ) (VAR x ) (RULES g(b) -> g(f(f(f(f(b))))) f(f(x)) -> b f(b) -> b g(f(b)) -> c h(x,g(b)) -> h(c,c) h(c,x) -> h(c,g(f(f(b)))) )