Confluence Competition

Categories – SRS

This category is concerned with confluence of string rewrite systems.


The input is a string rewrite system, specified in the specified in the ARI TRS format. The question to be answered is whether the string rewrite system is confluent.


  1. (format TRS)
    (fun f 1)
    (fun g 1)
    (rule (f (f x)) (g x))
    The correct answer is NO.
  2. (format TRS)
    (fun f 1)
    (rule (f (f x)) x)
    (rule (f x) (f (f x)))
    The correct answer is YES.

Problem Selection

Problems are selected from those in the ARI database with the 'srs' tag.