Categories – LCTRS

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

Format

The input is an logically constrained term rewrite systems, specified in the ARI LCTRS format. The question to be answered is whether the rewrite system is confluent.

Examples

1. (format LCTRS :smtlib 2.6)
   (theory Ints)
   (define-fun isEven ((x Int)) Bool (= (mod x 2) 0))
   (sort NList)
   (fun build (-> Int NList NList)) 
   (fun nats NList)
   (fun cons (-> Int NList NList)) 
   (fun nil NList)
   (rule nats (build 0 nil))
   (rule (build n xs) (build (+ n 1) (cons n xs)) :guard (and (isEven n) (>= n 0)))
   (rule (build n xs) (build (+ n 1) xs) :guard (and (not (isEven n)) (>= n 0)))
   

   The correct answer is YES.

2. ; @doi 10.1007/978-3-031-38499-8_27
   ; Example 3
   (format LCTRS :smtlib 2.6)
   (theory Ints)
   (fun f (-> Int Int))
   (rule (f x) z :guard (= x (* z z)) :var ((x Int) (z Int)))
   

   The correct answer is NO.

Problem Selection

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