Categories – CTRS

The CTRS category is concerned with confluence of conditional term rewrite systems.

Format

The input is an oriented conditional term rewrite system of type 3, specified in the ARI CTRS format. The question to be answered is whether the rewrite system is confluent.

Examples

1. (format CTRS oriented)
   (fun false 0)
   (fun not 1)
   (fun true 0)
   (rule (not x) false (= x true))
   (rule (not x) true (= x false))
   

   The correct answer is YES.

2. (format CTRS oriented)
   (fun a 0)
   (fun b 0)
   (fun c 0)
   (rule a b)
   (rule a c)
   (rule b c (= b c))
   

   The correct answer is NO.

Problem Selection

Problems are selected from those in the ARI database with the 'type3' and 'oriented' tags.