Categories – GCR

The GCR category is concerned with ground-confluence of many-sorted term rewrite systems (MSTRSs)

Format

The input is a many-sorted first-order rewrite system without conditions, specified in the MSTRS format. The question to be answered is whether the rewrite system is confluent on all well-sorted ground terms.

Examples

1. (format MSTRS)
   (sort 0)
   (sort 1)
   (fun a 0)
   (fun b 0)
   (fun c 0)
   (fun f (-> 0 0 1))
   (rule a b)
   (rule (f b b) (f a a))
   (rule (f x a) (f a a))
   

   The correct answer is NO.

2. (format MSTRS)
   (sort Nat)
   (sort Bool)
   (fun 0 Nat)
   (fun s (-> Nat Nat))
   (fun eq (-> Nat Nat Bool))
   (fun true Bool)
   (fun false Bool)
   (rule (eq x x) true)
   (rule (eq 0 (s x)) false)
   (rule (eq (s x) 0) false)
   (rule (eq (s x) (s y)) (eq x y))
   (rule (eq x y) (eq y x))
   

   The correct answer is YES.

Problem Selection

Problems are selected from those in the ARI database with the 'trs' or the 'mstrs' tag. The former are transformed into MSTRSs with a single sort, prior to passing them to tools.