predicates.clj

;; Using https://github.com/frenchy64/Logic-Starter/blob/master/src/logic_introduction/decl_model.clj

;; Without delving particularly into first order logic theory, we can see that
;; a building block of LP is the predicate.

(defn append-iio [a b c]
  (match [a b c]
         [[] _ _] (set-or-equals c b)
         [[x & as] _ _] (let-dataflow [cs]
                          (choose-all
                            (append-iio as b cs)
                            (set-or-equals c (cons x (deref cs)))))))


logic-introduction.decl-model=> (append-iio [1] [2] [1 2])
true
logic-introduction.decl-model=> (append-iio [1] [2] [1])
false
logic-introduction.decl-model=> (solve-dataflow [q]
                                  (append-iio [1] [2] q))
(1 2)
logic-introduction.decl-model=> (solve-dataflow [q]
                                  (append-iio [1] [2] []))
:logic-introduction.decl-model/NORESULT
logic-introduction.decl-model=> (solve-dataflow [q]
                                  (append-iio [1] [2] [1 2]))
:logic-introduction.decl-model/UNBOUND-DATAFLOW


(defn person [x]
  (choose-one
    ((undo-if-false [x]
       (set-or-equals x 'john)))
    ((undo-if-false [x]
       (set-or-equals x 'andrew)))
    ((undo-if-false [x]
       (set-or-equals x 'james)))))



logic-introduction.decl-model=> (person 'john)
true
logic-introduction.decl-model=> (person 'a)
false
logic-introduction.decl-model=> (solve-dataflow [q]
                                  (person q))
john
logic-introduction.decl-model=> (solve-dataflow [q]
                                  (person 'andrew))
:logic-introduction.decl-model/UNBOUND-DATAFLOW