Examples

A classic AI program:

(ns classic-ai-example
   (:refer-clojure :exclude [==])
   (:use clojure.core.logic))

(defne moveo [before action after]
  ([[:middle :onbox :middle :hasnot]
    :grasp
    [:middle :onbox :middle :has]])
  ([[pos :onfloor pos has]
    :climb
    [pos :onbox pos has]])
  ([[pos1 :onfloor pos1 has]
    :push
    [pos2 :onfloor pos2 has]])
  ([[pos1 :onfloor box has]
    :walk
    [pos2 :onfloor box has]]))

(defne cangeto [state out]
  ([[_ _ _ :has] true])
  ([_ _] (fresh [action next]
           (moveo state action next)
           (cangeto next out))))

(run 1 [q]
  (cangeto [:atdoor :onfloor :atwindow :hasnot] q)) ; (true)

Sudoku

(ns sudoku
  (:refer-clojure :exclude [==])
  (:use clojure.core.logic))

(defn get-square [rows x y]
  (for [x (range x (+ x 3))
        y (range y (+ y 3))]
    (get-in rows [x y])))

(defn init [vars hints]
  (if (seq vars)
    (let [hint (first hints)]
      (all
        (if-not (zero? hint)
          (== (first vars) hint)
          succeed)
        (init (next vars) (next hints))))
    succeed))

(defn sudokufd [hints]
  (let [vars (repeatedly 81 lvar) 
        rows (->> vars (partition 9) (map vec) (into []))
        cols (apply map vector rows)
        sqs  (for [x (range 0 9 3)
                   y (range 0 9 3)]
               (get-square rows x y))]
    (run 1 [q]
      (== q vars)
      (everyg #(infd % (domain 1 2 3 4 5 6 7 8 9)) vars)
      (init vars hints)
      (everyg distinctfd rows)
      (everyg distinctfd cols)
      (everyg distinctfd sqs))))

A type inferencer for the simply typed lambda calculus

(ns simple-typed-lambda-calculus
   (:refer-clojure :exclude [==])
   (:use clojure.core.logic))

(defna findo [x l o]
  ([_ [[y :- o] . _] _] 
    (project [x y] (== (= x y) true)))
  ([_ [_ . c] _] (findo x c o)))

(defn typedo [c x t]
  (conda
    [(lvaro x) (findo x c t)]
    [(matche [c x t]
       ([_ [[y] :>> a] [s :> t]]
          (fresh [l]
            (conso [y :- s] c l)
            (typedo l a t)))
       ([_ [:apply a b] _]
          (fresh [s]
            (typedo c a [s :> t])
            (typedo c b s))))]))

(comment
  ;; ([_.0 :> _.1])
  (run* [q]
    (fresh [f g a b t]
     (typedo [[f :- a] [g :- b]] [:apply f g] t)
     (== q a)))

  ;; ([:int :> _.0])
  (run* [q]
    (fresh [f g a t]
     (typedo [[f :- a] [g :- :int]] [:apply f g] t)
     (== q a)))

  ;; (:int)
  (run* [q]
    (fresh [f g a t]
     (typedo [[f :- [:int :> :float]] [g :- a]] 
       [:apply f g] t)
     (== q a)))

  ;; ()
  (run* [t]
    (fresh [f a b]
      (typedo [f :- a] [:apply f f] t)))

  ;; ([_.0 :> [[_.0 :> _.1] :> _.1]])
  (run* [t]
    (fresh [x y]
      (typedo [] 
        [[x] :>> [[y] :>> [:apply y x]]] t)))
  )