tlp.clj

; Temporal logic programming with explicit time using core.logic
; we assume relations s, <o and constants zero, one, four are defined as in
; https://github.com/frenchy64/Logic-Starter/blob/master/src/logic_introduction/numbers.clj

; we start by using 'next' to define a Fibonacci relation
; that is equal to F(n) at time n

; We use the small trick that if a number
; has a predecessor and then another, then it is at least 2
(defn fib [v t]
  (conde
   ((== t zero) (== v 0))
   ((== t one)  (== v 1))
   ((fresh [p pp x y]
           (s p t)
           (s pp p)
           (fib x p)
           (fib y pp)
           (project [x y]
                    (== v (+ x y)))))))

(run* [q] (fib q four))
;=> (3)

(run 10 [q] (fresh [v t] (fib v t) (== q [t v])))
;=> ([0 0] [(0) 1] [((0)) 1] [(((0))) 2] [((((0)))) 3]
; [(((((0))))) 5] [((((((0)))))) 8] [(((((((0))))))) 13]
; [((((((((0)))))))) 21] [(((((((((0))))))))) 34])

; Is a fibonacci number eventually bigger than 10?
(run 1 [q]
      (fresh [v t]
             (fib v t)
             (project [v]
                      (if (> v 10) succeed fail))))
;=> (_.0)

; Always true past t = 4
(defn pastfour [t]
  (<o four t))