* Category type demonstration category for CoCo 2015 * Problem and Semantics Our problem is to check ground confluence of many-sorted term rewriting systems. A many-sorted term rewriting system R is ground confluent if the rewrite relation ->R is confluent on the set of ground terms. For many-sorted term rewriting systems, 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 term rewrite system. To declare many-sorted term rewrite system, we add the following changes to the specification of first-order TRS (in old TPDB format): (i) Add sort to variable declaration. (ii) Add sorted function declaration. Thus, decl is replaced as follows: ........... decl ::= VAR varlist | RULES listofrules | FUN funlist | id anylist funlist ::= id : sort varlist ::= id : id sort ::= id | idlist -> id idlist ::= id | id , idlist ........... Furthermore, id should not contain ':'. * Example (FUN plus : Nat, Nat -> Nat s : Nat -> Nat 0 : Nat ) (VAR x : Nat y : Nat ) (RULES plus(0,0) -> 0 plus(s(x),y) -> s(plus(x,y)) plus(x,s(y)) -> s(plus(y,x)) )