Skip to content
This repository


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Fetching latest commit…

Cannot retrieve the latest commit at this time


A Logic Programming library for Clojure. At its heart is an original implementation of miniKanren as described in William Byrd's dissertation Relational Programming in miniKanren: Techniques, Applications, and Implementations. It's also described in great detail in the The Reasoned Schemer. However, do note that the version that appears in The Reasoned Schemer is an earlier implementation and differs from the one on which this library is based.

Performance is a central concern of this project. Anything that makes it slower will probably not be adopted. Anything that makes it faster without overly complicating the implementation will be considered. It would be interesting to see how we fare on the standard Prolog benchmarks. Currently, on my machine, solving the classic Zebra puzzle 1000 times takes SWI-Prolog about 6 seconds, it takes core.logic running under Clojure 1.3.0-alpha7 less then 2s without occurs-check.

If you wish to work through The Reasoned Schemer with core.logic make sure to look over this first.


A classic AI program:

(use '[clojure.core.logic minikanren prelude])

(defne moveo [before action after]
  ([[:middle :onbox :middle :hasnot]
    [:middle :onbox :middle :has]])
  ([[?pos :onfloor ?pos ?has]
    [?pos :onbox ?pos ?has]])
  ([[?pos1 :onfloor ?pos1 ?has]
    [?pos2 :onfloor ?pos2 ?has]])
  ([[?pos1 :onfloor ?box ?has]
    [?pos2 :onfloor ?box ?has]]))

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

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

A classic Prolog program:

append([] ,Y,Y).
append([A|D],Y2,[A|R]) :- append(D,Y2,R).

The core.logic version is almost equally succinct:

(defne appendo [x y z]
  ([() _ y])
  ([[?a . ?d] _ [?a . ?r]] (appendo ?d y ?r)))

Here's a simple type inferencer for the simply typed lambda calculus based on a version originally written in Prolog:

(use '[clojure.core.logic minikanren prelude nonrel match])

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

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

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

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

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

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

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


core.logic as of version 0.5.4 supports tabling. Certain kinds of logic programs that would not terminate in Prolog will terminate in core.logic if you create a tabled goal.

(defne arco [x y]
  ([:a :b])
  ([:b :a])
  ([:b :d]))

(def patho
  (tabled [x y]
     ((arco x y))
     ((exist [z]
        (arco x z)
        (patho z y))))))

;; (:b :a :d)
(run* [q] (patho :a q))


core.logic supports disequality constraints.

(run* [q]
  (exist [x y]
    (!= [x 2] [y 1])
    (== x 1)
    (== y 3)
    (== q [x y]))) ; ([1 3])

(run* [q]
  (exist [x y]
    (!= [x 2] [y 1])
    (== x 1)
    (== y 2)
    (== q [x y]))) ; ()


core.logic comes with a unifier that can be used much like core.unify:

(unifier '(?x ?y ?z) '(1 2 ?y)) ; (1 2 _.0)

The above is quite slow since we have to walk the data structure and replace the logic var symbols. It's more efficient to prep the expressions before hand if you're going to be unifying the same expressions over and over again.

(let [[u w] (map prep ['(?x ?y) (1 2)])]
  (unifier* u w))

Definite Clause Grammars

core.logic has Prolog-type DCG syntax for parsing:

(def-->e verb [v]
  ([[:v 'eats]] '[eats]))

(def-->e noun [n]
  ([[:n 'bat]] '[bat])
  ([[:n 'cat]] '[cat]))

(def-->e det [d]
  ([[:d 'the]] '[the])
  ([[:d 'a]] '[a]))

(def-->e noun-phrase [n]
  ([[:np ?d ?n]] (det ?d) (noun ?n)))

(def-->e verb-phrase [n]
  ([[:vp ?v ?np]] (verb ?v) (noun-phrase ?np)))

(def-->e sentence [s]
  ([[:s ?np ?vp]] (noun-phrase ?np) (verb-phrase ?vp)))

(run* [parse-tree]
  (sentence parse-tree '[the bat eats a cat] []))

;; ([:s [:np [:d the] [:n bat]] [:vp [:v eats] [:np [:d a] [:n cat]]]])

Defining facts

Sometimes it's useful to create a list of facts that you want to run queries over. Use defrel and fact.

(defrel man p)
(fact man 'Bob)
(fact man 'John)
(fact man 'Ricky)

(defrel woman p)
(fact woman 'Mary)
(fact woman 'Martha)
(fact woman 'Lucy)

(defrel likes p1 p2)
(fact likes 'Bob 'Mary)
(fact likes 'John 'Martha)
(fact likes 'Ricky 'Lucy)

(defrel fun p)
(fact fun 'Lucy)

(run* [q]
  (exist [x y]
    (fun y)
    (likes x y)
    (== q [x y]))) ; ([Ricky Lucy])

It's important to index relationships so that the time to run queries doesn't grow linearly with the number of facts. You can create indexes for any element of the fact tuple. Note that this has implications for memory usage.

; Clojure 1.3.0
(defrel likes ^:index p1 ^:index p2)

; Clojure 1.2.0
(defrel likes ^{:index true} p1 ^{:index true} p2)


The core Prolog aspect of core.logic is nearing completion. The following are tentative future directions:

  • Negation - Stratified Negation as provided by XSB ?
  • Definite Clause Grammar
  • Constraint Logic Programming - Constraint Handling Rules (CHR) is particularly inspiring


YourKit has has given me a free license for their profiler, greatly simplifying the profiling of core.logic performance.



I stayed pretty true to the ideas of the original implementation. There are however several key differences. Unification uses protocols in order leverage the full speed of the host. Clojure's cons operator differs significantly from Scheme's so I added the LConsSeq protocol. Sequences which end in a logic variables can be represented by using lcons

(lcons 'a (lvar 'b)) ; (a . <lvar:b>)

Logic variables are instances of LVar not vectors as they are in Scheme.

The goal and goal constructor portion has been written from scratch on top of the protocols and makes liberal use of lazy sequences to prevent stack overflow.

Currently the Substitutions deftype uses clojure.lang.PersistentHashMap internally. This may be replaced with something that provides better performance for triangular substitutions.


  • Simplicity. Optimizations should not destroy the ideas behind the original design. Any person willing to take take the time to understand the original Scheme implementation should have little trouble understanding how core.logic is put together.
  • Performance. This implementation is faster than miniKanren under Racket and seems to be close to performnace of miniKanren recorded by the original designers when running under Chez Scheme.
  • Emphasis on pure relational programming.


Distributed under the Eclipse Public License, the same as Clojure.

Something went wrong with that request. Please try again.