some kind of tests for rules

doc/intro.md

@@ -1,3 +0,0 @@
-# Introduction to narjure
-
-TODO: write [great documentation](http://jacobian.org/writing/what-to-write/)

project.clj

@@ -14,7 +14,8 @@
   :plugins [[lein-cloverage "1.0.6"]
             [jonase/eastwood "0.2.3"]
             [lein-kibit "0.1.2"]
-            [cider/cider-nrepl "0.11.0-SNAPSHOT"]]
+            [cider/cider-nrepl "0.11.0-SNAPSHOT"]
+            [michaelblume/lein-marginalia "0.9.0"]]
   :eastwood {:exclude-namespaces [nal.rules]}
   :target-path "target/%s"
   :repl-options {:init-ns          narjure.repl

resources/narsese.bnf

@@ -2,7 +2,7 @@
 
              task ::= [budget] sentence                       (* task to be processed *)
 
-         sentence ::= statement"." [tense] [truth]            (* judgement to be remembered *)
+         sentence ::= statement"." [tense] [truth]            (* belief to be remembered *)
                     | statement"?" [tense] [truth]            (* question to be answered, tense added in OpenNARS 1.7 *)
                     | statement"@" [tense] [truth]            (* question on desire value to be answered, tense added in OpenNARS 1.7 *)
                     | statement"!" [tense] [truth]            (* goal to be realized, tense added in OpenNARS 1.7 *)

src/nal/core.clj

@@ -7,12 +7,8 @@
   (if (>= c1 c2) [f1 c1] [f2 c2]))
 
 (defn inference
-  [{:keys [task-type] :as task} belief]
-  (generate-conclusions (r/rules task-type) task belief))
+  ([task belief] (inference r/rules task belief))
+  ([rules {:keys [task-type] :as task} belief]
+   (generate-conclusions (rules task-type) task belief)))
 
 (def revision t/revision)
-
-(comment
-  :shift-occurrence-forward                                 ;pre
-  :shift-occurrence-backward                                 ;pre
-  :linkage-temporal)

src/nal/deriver/backward_rules.clj

@@ -1,6 +1,7 @@
 (ns nal.deriver.backward-rules
   (:require [nal.deriver.key-path :refer [rule-path]]
-            [clojure.string :as s]))
+            [clojure.string :as s]
+            [nal.deriver.utils :as u]))
 
 ;http://pastebin.com/3zLX7rPx
 (defn allow-backward?
@@ -29,22 +30,25 @@
   "If rule allows backward inference it will be expanded to three rules,
   where first one is the rule itself, and rest rules will be generated by
   swapping conclusion with every premise."
-  [{:keys [p1 p2 conclusions pre] :as rule}]
+  [{:keys [p1 p2 conclusions pre id] :as rule}]
   (mapcat (fn [{:keys [conclusion post] :as fc}]
             (let [post (reduce #(remove (partial has-prefix? %2) %1)
                                post [":t/" ":d/"])]
               (conj (map
                       (fn [r] (update r :pre conj :question?))
-                      [(assoc rule :conclusions [(assoc fc :post post)])
+                      [(assoc rule :conclusions [(assoc fc :post post)]
+                                   :id (u/concat-kw id :q))
                        (assoc rule :p1 conclusion
                                    :conclusions [{:conclusion p1
                                                   :post       post}]
                                    :full-path (rule-path conclusion p2)
-                                   :pre (check-not-equal pre p1))
+                                   :pre (check-not-equal pre p1)
+                                   :id (u/concat-kw id :backward1))
                        (assoc rule :p2 conclusion
                                    :conclusions [{:conclusion p2
                                                   :post       post}]
                                    :full-path (rule-path p1 conclusion)
-                                   :pre (check-not-equal pre p2))])
+                                   :pre (check-not-equal pre p2)
+                                   :id (u/concat-kw id :backward2))])
                     rule)))
           conclusions))

src/nal/deriver/list_expansion.clj

@@ -1,6 +1,7 @@
 (ns nal.deriver.list-expansion
   (:require [nal.deriver.utils :refer [walk]]
-            [clojure.string :as s]))
+            [clojure.string :as s]
+            [nal.deriver.utils :as u]))
 
 (def max-elements-in-list 7)
 
@@ -36,18 +37,26 @@
   "Expands :from/ element in rule, so as a result will be created n rules, in
   each of them :form/A will be replaced with A1 or A2 or A3, etc."
   [statement from-name list-name n]
-  (map (fn [idx]
-         (walk statement
-           (= from-name el) (symbol (str list-name idx))))
-       (range 1 (inc n))))
+  (let [st (butlast statement)
+        id (last statement)]
+    (map (fn [idx]
+           (let [sym (str list-name idx)
+                 new-id (u/concat-kw id sym)]
+             (walk (concat st [new-id])
+               (= from-name el) (symbol sym))))
+         (range 1 (inc n)))))
 
 (defn generate-all-lists
   "Expands rules with :list/ elements, as a result will be created 5 rules,
   where :list/ will be replaced with A1, A1 A2, ..., A1..A5."
   [r]
   (let [list (get-list ":list" r)
-        l-name (list-name list)]
-    (mapcat #(let [st (replace-list-elemets r list l-name %)]
+        l-name (list-name list)
+        id (last r)
+        r-without-id (butlast r)]
+    (mapcat #(let [new-id (u/concat-kw id (str l-name %))
+                   r (concat r-without-id [new-id])
+                   st (replace-list-elemets r list l-name %)]
               (if-let [from-name (get-list ":from" st)]
                 (expand-:from-element st from-name l-name %)
                 [st]))

src/nal/deriver/matching.clj

@@ -50,14 +50,14 @@
 (defn form-conclusion
   "Formation of cocnlusion in terms of task and truth/desire functions"
   [{:keys [t1 t2 task-type]}
-   {c  :statement tf :t-function pj :p/judgement df :d-function
+   {c  :statement tf :t-function pj :p/belief df :d-function
     sc :shift-conditions}]
-  (let [conclusion-type (if pj :judgement task-type)
+  (let [conclusion-type (if pj :belief task-type)
         conclusion {:statement  c
                     :task-type  conclusion-type
                     :occurrence :t-occurrence}
         conclusion (case conclusion-type
-                     :judgement (assoc conclusion :truth (list tf t1 t2))
+                     :belief (assoc conclusion :truth (list tf t1 t2))
                      :goal (assoc conclusion :desire (list df t1 t2))
                      conclusion)]
     (if sc
@@ -267,7 +267,7 @@
                                       sym-map)
                   :t-function       (t/tvtypes (get-truth-fn post))
                   :d-function       (t/dvtypes (get-desire-fn post))
-                  :p/judgement      (some #{:p/judgement} post)}
+                  :p/belief      (some #{:p/belief} post)}
      :conditions (remove nil?
                          (walk (concat (check-conditions sym-map) pre)
                            (and (coll? el) (= \a (first (str (first el)))))

src/nal/deriver/premises_swapping.clj

@@ -1,10 +1,11 @@
 (ns nal.deriver.premises-swapping
   (:require [nal.deriver.key-path :refer [rule-path]]
-            [nal.deriver.normalization :refer [commutative-ops]]))
+            [nal.deriver.normalization :refer [commutative-ops]]
+            [nal.deriver.utils :as u]))
 
 ;the set of keys which prevent premises swapping for rule
 (def anti-swapping-keys
-  #{:question? :judgement? :goal? :measure-time :t/belief-structural-deduction
+  #{:question? :belief? :goal? :measure-time :t/belief-structural-deduction
     :t/structural-deduction :t/belief-structural-difference :t/identity
     :t/negation :union :intersection :t/intersection :t/union})
 
@@ -16,9 +17,10 @@
          (not-any? commutative-ops (flatten conclusion)))))
 
 (defn swap-premises
-  [{:keys [p1 p2] :as rule}]
+  [{:keys [p1 p2 id] :as rule}]
   (assoc rule :p1 p2
               :p2 p1
-              :full-path (rule-path p2 p1)))
+              :full-path (rule-path p2 p1)
+              :id (u/concat-kw id :swap)))
 
 (defn swap [rule] [rule (swap-premises rule)])

src/nal/deriver/rules.clj

@@ -1,15 +1,17 @@
 (ns nal.deriver.rules
   (:require [clojure.string :as s]
             [clojure.set :refer [map-invert]]
+            [clojure.core.match :as m]
             [nal.deriver
              [key-path :refer [rule-path all-paths path-invariants path]]
-             [utils :refer [walk]]
+             [utils :refer [walk concat-kw]]
              [list-expansion :refer [contains-list? generate-all-lists]]
              [premises-swapping :refer [allow-swapping? swap]]
              [matching :refer [generate-matching]]
              [backward-rules :refer [allow-backward? expand-backward-rules]]
              [normalization :refer [infix->prefix replace-negation]]
-             [terms-permutation :refer [order-for-all-same? generate-all-orders]]]))
+             [terms-permutation :refer [order-for-all-same? generate-all-orders]]]
+            [nal.deriver.utils :as u]))
 
 (defn options
   "Generates map from rest of the rule's args."
@@ -24,29 +26,48 @@
     (map (fn [[c _ post]] {:conclusion c :post post}) (partition 3 c))
     [{:conclusion c :post (:post opts)}]))
 
+(defn rule*
+  ([p1 p2 c other] (rule* p1 p2 c other ""))
+  ([p1 p2 c other pf]
+   (let [p1 (infix->prefix p1)
+         p2 (infix->prefix p2)
+         c (infix->prefix c)
+         opts (options other)
+         conclusions (get-conclusions c opts)
+         id (concat-kw (opts :id) pf)
+         cnt (count conclusions)]
+     (for [n (range 0 cnt)]
+       {:p1          p1
+        :p2          p2
+        :conclusions [(nth conclusions n)]
+        :full-path   (rule-path p1 p2)
+        :pre         (infix->prefix (:pre opts))
+        :origin      (opts :origin)
+        :id          (if (zero? n)
+                       id
+                       (u/concat-kw id (str (inc n))))}))))
+
+(defn get-second-premises [p1]
+  (m/match (vec p1)
+    [_ ([fp2 _ sp2] :seq)] [fp2 sp2]
+    [fp2 _ sp2] [fp2 sp2]))
+
 (defn rule
   "Generates rule from #R statement."
   [data]
-  (let [[p1 p2 _ c & other] (replace-negation data)]
-    (let [p1 (infix->prefix p1)
-          p2 (infix->prefix p2)
-          c (infix->prefix c)
-          opts (options other)
-          conclusions (get-conclusions c opts)]
-      (map (fn [c]
-             {:p1          p1
-              :p2          p2
-              :conclusions [c]
-              :full-path   (rule-path p1 p2)
-              :pre         (infix->prefix (:pre opts))})
-           conclusions))))
+  (m/match (vec (replace-negation data))
+    [p1 '|- c & other]
+    (let [[fp2 sp2] (get-second-premises p1)]
+      (concat (rule* p1 fp2 c other :prem1)
+              (rule* p1 sp2 c other :prem2)))
+    [p1 p2 '|- c & other] (rule* p1 p2 c other)))
 
 (defn check-duplication
   "Checks if there are rules with same premises and preconditions but with
   different conclusions, merges them if they exist."
   [rules]
-  (vals (reduce (fn [ac {:keys [p1 p2 pre conclusions] :as r}]
-                  (let [k [p1 p2 pre]]
+  (vals (reduce (fn [ac {:keys [p1 p2 pre conclusions id origin] :as r}]
+                  (let [k [p1 p2 (set pre)]]
                     (if (ac k)
                       (update-in ac [k :conclusions] concat conclusions)
                       (assoc ac k r))))
@@ -71,26 +92,11 @@
                           (s/starts-with? (str el) ":d/")))
             post)))
 
-(defn judgement?
-  "Return true if rule allows only judgement as task."
+(defn belief?
+  "Return true if rule allows only belief as task."
   [{:keys [pre] :as rule}]
   (not (or (question? rule) (some #{:goal} pre))))
 
-(defn add-possible-paths
-  "Selects all rules that will match the same path as current rule and adds
-  these rules to the set of rules that matches path.
-  For instance:
-  current rule's path [[--> [- :any :any] :any] :and [--> [:any :any]]]
-
-  so, if we find rule with path [[--> :any :any] :and [--> [:any :any]]],
-  it matches to current's rule path too, hence it should be added to the set
-  of rules that matches [[--> [- :any :any] :any] :and [--> [:any :any]]] path."
-  [ac [k {:keys [all]}]]
-  (let [rules (mapcat :rules (vals (select-keys ac all)))]
-    (-> ac
-        (update-in [k :rules] concat rules)
-        (update-in [k :rules] set))))
-
 (defn rule->map
   "Adds rule to map of rules, conjoin rule to set of rules that
   matches to pattern. Rules paths are keys in this map."
@@ -123,30 +129,36 @@
             `~raw-rules
             pairs)))
 
-(defmacro defrules [name & rules]
+(defmacro defrules [name rules]
   `(def ~name (quote ~rules)))
 
+(defn expand-rules [rules]
+  (rules->> (apply concat rules)
+            contains-list? generate-all-lists
+            contains-list? generate-all-lists
+            identity rule
+            order-for-all-same? generate-all-orders
+            allow-swapping? swap
+            allow-backward? expand-backward-rules))
+
+(defn generate-deriver [expanded-rules]
+  (let [judgement-rules# (check-duplication (filter belief? expanded-rules))
+        question-rules# (check-duplication (filter question? expanded-rules))
+        goal-rules# (check-duplication (filter goal? expanded-rules))
+        quest-rules# (check-duplication (filter quest? expanded-rules))]
+    (println "Beliefs rules:" (count judgement-rules#))
+    (println "Questions rules:" (count question-rules#))
+    (println "Goal rules:" (count goal-rules#))
+    (println "Quests rules:" (count quest-rules#))
+    {:belief   (rules-map judgement-rules# :belief)
+     :question (rules-map question-rules# :question)
+     :goal     (rules-map goal-rules# :goal)
+     :quest    (rules-map quest-rules# :quest)
+     :origin   (group-by :origin expanded-rules)
+     :id       (group-by :id expanded-rules)}))
+
 (defn compile-rules
   "Define rules. Rules must be #R statements."
   ;TODO exception on duplication of the rule
   [& rules]
-  (time
-    (let [rules (rules->> (apply concat rules)
-                          contains-list? generate-all-lists
-                          contains-list? generate-all-lists
-                          identity rule
-                          order-for-all-same? generate-all-orders
-                          allow-swapping? swap
-                          allow-backward? expand-backward-rules)
-          judgement-rules# (check-duplication (filter judgement? rules))
-          question-rules# (check-duplication (filter question? rules))
-          goal-rules# (check-duplication (filter goal? rules))
-          quest-rules# (check-duplication (filter quest? rules))]
-      (println "Beliefs rules:" (count judgement-rules#))
-      (println "Questions rules:" (count question-rules#))
-      (println "Goal rules:" (count goal-rules#))
-      (println "Quests rules:" (count quest-rules#))
-      {:judgement (rules-map judgement-rules# :judgement)
-       :question  (rules-map question-rules# :question)
-       :goal      (rules-map goal-rules# :goal)
-       :quest     (rules-map quest-rules# :quest)})))
+  (time (generate-deriver (expand-rules rules))))

src/nal/deriver/terms_permutation.clj

@@ -1,5 +1,6 @@
 (ns nal.deriver.terms-permutation
-  (:require [nal.deriver.utils :refer [walk]]))
+  (:require [nal.deriver.utils :refer [walk]]
+            [nal.deriver.utils :as u]))
 
 (defn contains-op?
   "Checks if statement contains operators from set."
@@ -17,11 +18,28 @@
   [statement from to]
   (walk statement (= from el) to))
 
+(def names
+  {'conj       :conj
+   '&|         :parallel-conj
+   'seq-conj   :seq-conj
+   '<=>        :equiv
+   '</>        :pred-equiv
+   '<|>        :conc-equiv
+   '==>        :impl
+   'pred-impl  :pred-impl
+   '=|>        :concur-impl
+   'retro-impl :retro-impl})
+
 (defn permute-op
   "Makes permuatation of operators from s in statement."
   [statement s]
   (if-let [op (contains-op? statement s)]
-    (map #(replace-op statement op %) s)
+    (let [id (last statement)
+          st (butlast statement)]
+      (map (fn [new-op]
+             (let [new-id (u/concat-kw id :perm (names new-op))]
+               (replace-op (concat st [new-id]) op new-op)))
+           s))
     [statement]))
 
 ;equivalences, implications, conjunctions - sets of operators that are use in
@@ -32,18 +50,21 @@
 
 (defn generate-all-orders
   "Permutes all operators in statement with :order-for-all-same precondition."
-  [{:keys [p1 p2 conclusions full-path pre] :as rule}]
+  [{:keys [p1 p2 conclusions full-path pre id origin] :as rule}]
   (let [{:keys [conclusion] :as c1} (first conclusions)
-        statements (->> (permute-op [p1 p2 conclusion full-path pre] equivalences)
-                        (mapcat (fn [st] (permute-op st conjunctions)))
-                        (mapcat (fn [st] (permute-op st implications)))
-                        set)]
-    (map (fn [[p1 p2 c full-path pre]]
+        statements
+        (->> (permute-op [p1 p2 conclusion full-path pre id] equivalences)
+             (mapcat (fn [st] (permute-op st conjunctions)))
+             (mapcat (fn [st] (permute-op st implications)))
+             set)]
+    (map (fn [[p1 p2 c full-path pre id]]
            (assoc rule :p1 p1
                        :p2 p2
                        :full-path full-path
                        :conclusions [(assoc c1 :conclusion c)]
-                       :pre pre))
+                       :pre pre
+                       :id id
+                       :origin origin))
          statements)))
 
 (defn order-for-all-same?

src/nal/deriver/truth.clj

@@ -94,11 +94,11 @@
 (defn difference [[^double f1 ^double c1] [^double f2 ^double c2]]
   [(t-and f1 (- 1 f2)) (t-and c1 c2)])
 
-(defn structual-intersection [_ p2] (deduction p2 [1 d/judgement-confidence]))
+(defn structual-intersection [_ p2] (deduction p2 [1 d/belief-confidence]))
 
-(defn structual-deduction [p1 _] (deduction p1 [1 d/judgement-confidence]))
+(defn structual-deduction [p1 _] (deduction p1 [1 d/belief-confidence]))
 
-(defn structual-abduction [p1 _] (abduction p1 [1 d/judgement-confidence]))
+(defn structual-abduction [p1 _] (abduction p1 [1 d/belief-confidence]))
 
 (defn reduce-conjunction [p1 p2]
   (-> (negation p1 p2)
@@ -113,11 +113,11 @@
 (defn belief-identity [p1 p2] (when p2 p1))
 
 (defn belief-structural-deduction [_ p2]
-  (when p2 (deduction p2 [1 d/judgement-confidence])))
+  (when p2 (deduction p2 [1 d/belief-confidence])))
 
 (defn belief-structural-difference [_ p2]
   (when p2
-    (let [[^double f ^double c] (deduction p2 [1 d/judgement-confidence])]
+    (let [[^double f ^double c] (deduction p2 [1 d/belief-confidence])]
       [(- 1 f) c])))
 
 (defn belief-negation [_ p2] (when p2 (negation p2 nil)))
@@ -131,7 +131,7 @@
 
 (defn desire-structural-strong
   [t _]
-  (analogy t [1.0 d/judgement-confidence]))
+  (analogy t [1.0 d/belief-confidence]))
 
 (def tvtypes
   {:t/structural-deduction         structual-abduction

src/nal/deriver/utils.clj

@@ -1,5 +1,13 @@
 (ns nal.deriver.utils
-  (:require [clojure.walk :as w]))
+  (:require [clojure.walk :as w]
+            [clojure.string :as s]))
+
+(defn concat-kw [& kws]
+  (->> (remove nil? kws)
+       (map name)
+       (remove #{""})
+       (s/join "-")
+       keyword))
 
 (defn not-operator?
   "Checks if element is not operator"

src/nal/reader.clj

@@ -10,18 +10,6 @@
              nil)]
     (aset dm (int ch) fun)))
 
-(defn fetch-rule
-  ([rdr] (fetch-rule rdr "" 0))
-  ([rdr prev cnt]
-   (let [c (.read rdr)
-         cnt (case (char c)
-               \] (dec cnt)
-               \[ (inc cnt)
-               cnt)]
-     (if (neg? cnt)
-       prev
-       (recur rdr (str prev (char c)) cnt)))))
-
 (defn add-brackets [s]
   (str "[" s "]"))
 
@@ -47,10 +35,38 @@
 (defn read-rule [s]
   (-> s replacements add-brackets read-string))
 
-(defn rule [rdr letter-R opts & other]
-  (let [c (.read rdr)]
-    (if (= c (int \[))
-      (read-rule (fetch-rule rdr))
-      (throw (Exception. (str "Reader barfed on " (char c)))))))
+(defn fetch-rules
+  ([rdr] (fetch-rules rdr "" nil 0))
+  ([rdr prev prev-char cnt]
+   (let [n (.read rdr)
+         c (char n)]
+     (if (and (= c \#) (= \R prev-char))
+       prev
+       (recur rdr (str prev c) c cnt)))))
+
+(defn comment->key [comment]
+  (-> comment
+      (s/replace #"\s" "-")
+      (s/replace #";" "")
+      keyword))
+
+(defn rules [rdr _ _ & _]
+  (->> (reduce (fn [{:keys [prev-comment prev-not-comment]
+                     :as   ac} l]
+                 (if (or (s/starts-with? l ";")
+                         (s/starts-with? l "R"))
+                   (-> (assoc ac :prev-comment l
+                                 :prev-not-comment "")
+                       (update :rules conj {:comment prev-comment
+                                            :rule    prev-not-comment}))
+                   (update ac :prev-not-comment str l)))
+               {:prev-not-comment ""}
+               (map s/trim (s/split-lines (fetch-rules rdr))))
+       :rules
+       (remove (fn [{c :comment r :rule}] (or (nil? c) (empty? r))))
+       (map (fn [{:keys [comment rule]}]
+              (let [id (comment->key comment)]
+                (vec (concat (read-rule rule) [:origin id :id id])))))))
+
+(dispatch-reader-macro \R rules)
 
-(dispatch-reader-macro \R rule)

src/narjure/defaults.clj

@@ -1,18 +1,18 @@
 (ns narjure.defaults)
 
-(def judgement-frequency 1.0)
-(def judgement-confidence 0.9)
+(def belief-frequency 1.0)
+(def belief-confidence 0.9)
 
 (def truth-value
-  [judgement-frequency judgement-confidence])
+  [belief-frequency belief-confidence])
 
-(def judgement-priority 0.5)
-(def judgement-durability 0.8)
+(def belief-priority 0.5)
+(def belief-durability 0.8)
 ;todo clarify this
-(def judgement-quality 0.5)
+(def belief-quality 0.5)
 
-(def judgement-budget
-  [judgement-priority judgement-durability judgement-quality])
+(def belief-budget
+  [belief-priority belief-durability belief-quality])
 
 (def question-priority 0.5)
 (def question-durability 0.9)
@@ -20,14 +20,14 @@
 (def question-quality 0.5)
 
 (def question-budget
-  [judgement-priority judgement-durability judgement-quality])
+  [belief-priority belief-durability belief-quality])
 
 (def goal-confidence 0.9)
 (def goal-priority 0.5)
 (def goal-durability 0.8)
 
 (def budgets
-  {:judgement judgement-budget
+  {:belief belief-budget
    :question question-budget})
 
 (def ^{:type double} horizon 1)

src/narjure/narsese.clj

@@ -43,7 +43,7 @@
 (defn get-compound-term [[_ operator-srt]]
   (compound-terms operator-srt))
 
-(def actions {"." :judgement
+(def actions {"." :belief
               "?" :question})
 
 (def ^:dynamic *action* (atom nil))

test/nal/test/core.clj

@@ -9,12 +9,12 @@
                    [&| [--> [ext-set tim] [int-set driving]]]
                    [--> [ext-set tim] [int-set dead]]]
        :truth     [1.0 0.81]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1})
 
     '[{:statement [--> [ext-set tim] [int-set drunk]]
        :truth     [1 0.9]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
 
       {:statement [==> [&| [--> [ind-var X] [int-set drunk]] [--> [ind-var X] [int-set driving]]]
@@ -24,32 +24,32 @@
 
     '({:occurrence 1
        :statement  [&| a1 [--> [* a1 a2 a3] m]]
-       :task-type  :judgement
+       :task-type  :belief
        :truth      [1.0
                     0.81]}
        {:occurrence 1
         :statement  [--> a1 [ext-image m _ a2 a3]]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1
                      0.9]}
        {:occurrence 1
         :statement  [<|> a1 [--> [* a1 a2 a3] m]]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1.0
                      0.44751381215469616]}
        {:occurrence 1
         :statement  [=|> [--> [* a1 a2 a3] m] a1]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1
                      0.44751381215469616]}
        {:occurrence 1
         :statement  [=|> a1 [--> [* a1 a2 a3] m]]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1
                      0.44751381215469616]})
     '[{:statement [--> [* a1 a2 a3] m]
        :truth     [1 0.9]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
 
       {:statement a1
@@ -57,24 +57,24 @@
        :occurrence 0}]
 
     '[{:statement [=|> [--> [* a1 a2 a3] m] a1],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1 0.44751381215469616]}
       {:statement [<|> a1 [--> [* a1 a2 a3] m]],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1.0 0.44751381215469616]}
       {:statement [&| [--> [* a1 a2 a3] m] a1],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1.0 0.81]}
       {:statement [=|> a1 [--> [* a1 a2 a3] m]],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1 0.44751381215469616]}]
     '[{:statement a1
        :truth     [1 0.9]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
 
       {:statement [--> [* a1 a2 a3] m]
@@ -83,29 +83,29 @@
 
     '({:occurrence 1
        :statement  [&| a1 [conj a1 a2 a3]]
-       :task-type  :judgement
+       :task-type  :belief
        :truth      [1.0 0.81]}
        {:occurrence 1
         :statement  [<|> a1 [conj a1 a2 a3]]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1.0 0.44751381215469616]}
        {:occurrence 1
         :statement  [=|> [conj a1 a2 a3] a1]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1
                      0.44751381215469616]}
        {:occurrence 1
         :statement  [=|> a1 [conj a1 a2 a3]]
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1
                      0.44751381215469616]}
        {:occurrence 1
         :statement  a1
-        :task-type  :judgement
+        :task-type  :belief
         :truth      [1 0.44751381215469616]})
     '[{:statement [conj a1 a2 a3]
        :truth     [1 0.9]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
 
       {:statement a1
@@ -113,24 +113,24 @@
        :occurrence 0}]
 
     '[{:statement [=|> [--> M S] [[--> M S] [--> M P]]],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1 0.44751381215469616]}
       {:statement [<|> [--> M S] [[--> M S] [--> M P]]],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1.0 0.44751381215469616]}
       {:statement [&| [--> M S] [[--> M S] [--> M P]]],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1.0 0.81]}
       {:statement [=|> [[--> M S] [--> M P]] [--> M S]],
-       :task-type :judgement,
+       :task-type :belief,
        :occurrence 1,
        :truth [1 0.44751381215469616]}]
     '[{:statement [[--> M S] [--> M P]]
        :truth     [1 0.9]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
 
       {:statement [--> M S]
@@ -140,17 +140,17 @@
     '({:statement [conj [--> [dep-var Y] [int-set B]]
                    [==> [--> [ext-set A] [int-set Y]] [--> [dep-var Y] P]]]
        :truth     [1.0 0.81]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
        {:statement [==>
                     [conj [--> [ext-set A] [int-set Y]] [--> [ind-var X] [int-set B]]]
                     [--> [ind-var X] P]]
         :truth     [1 0.44751381215469616]
-        :task-type :judgement
+        :task-type :belief
         :occurrence 1})
     '[{:statement [==> [--> [ext-set A] [int-set Y]] [--> [ext-set A] P]]
        :truth     [1 0.9]
-       :task-type :judgement
+       :task-type :belief
        :occurrence 1}
 
       {:statement [--> [ext-set A] [int-set B]]

test/nal/test/deriver.clj

@@ -6,114 +6,114 @@
 (def result
   '({:statement  [</>
                   [seq-conj [--> chess competition] [:interval 1000]]
-                  [--> sport competition]],
-     :task-type  :judgement,
-     :occurrence 1000,
+                  [--> sport competition]]
+     :task-type  :belief
+     :occurrence 1000
      :truth      [1.0 0.44751381215469616]}
      {:statement  [seq-conj
                    [--> chess competition]
                    [:interval 1000]
-                   [--> sport competition]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [--> sport competition]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.81]}
      {:statement  [pred-impl
                    [seq-conj [--> chess competition] [:interval 1000]]
-                   [--> sport competition]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [--> sport competition]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
      {:statement  [retro-impl
                    [--> sport competition]
-                   [seq-conj [--> chess competition] [:interval 1000]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [seq-conj [--> chess competition] [:interval 1000]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [--> sport chess],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [--> sport chess]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [--> chess sport],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [--> chess sport]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [<=> [--> chess [ind-var X]] [--> sport [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [<=> [--> chess [ind-var X]] [--> sport [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.44751381215469616]}
-     {:statement  [conj [--> chess [dep-var Y]] [--> sport [dep-var Y]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [conj [--> chess [dep-var Y]] [--> sport [dep-var Y]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.81]}
-     {:statement  [<-> sport chess],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [<-> sport chess]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.44751381215469616]}
-     {:statement  [==> [--> chess [ind-var X]] [--> sport [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [==> [--> chess [ind-var X]] [--> sport [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [==> [--> chess [ind-var X]] [--> sport [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [==> [--> chess [ind-var X]] [--> sport [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [==> [--> sport [ind-var X]] [--> chess [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [==> [--> sport [ind-var X]] [--> chess [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [==> [--> sport [ind-var X]] [--> chess [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [==> [--> sport [ind-var X]] [--> chess [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
-     {:statement  [--> [int-dif chess sport] competition],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [--> [int-dif chess sport] competition]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [0.0 0.81]}
-     {:statement  [--> [| chess sport] competition],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [--> [| chess sport] competition]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.81]}
-     {:statement  [--> [int-dif sport chess] competition],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [--> [int-dif sport chess] competition]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [0.0 0.81]}
-     {:statement  [--> [ext-inter chess sport] competition],
-      :task-type  :judgement,
-      :occurrence 1000,
+     {:statement  [--> [ext-inter chess sport] competition]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.81]}
      {:statement  [pred-impl
                    [seq-conj [--> chess [ind-var X]] [:interval 1000]]
-                   [--> sport [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [--> sport [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
      {:statement  [</>
                    [seq-conj [--> chess [ind-var X]] [:interval 1000]]
-                   [--> sport [ind-var X]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [--> sport [ind-var X]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.44751381215469616]}
      {:statement  [retro-impl
                    [--> sport [ind-var X]]
-                   [seq-conj [--> chess [ind-var X]] [:interval 1000]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [seq-conj [--> chess [ind-var X]] [:interval 1000]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1 0.44751381215469616]}
      {:statement  [seq-conj
                    [--> chess [dep-var Y]]
                    [:interval 1000]
-                   [--> sport [dep-var Y]]],
-      :task-type  :judgement,
-      :occurrence 1000,
+                   [--> sport [dep-var Y]]]
+      :task-type  :belief
+      :occurrence 1000
       :truth      [1.0 0.81]}))
 
 (deftest test-generate-conclusions
   (is (= (set result)
          (set (generate-conclusions
-                (r/rules :judgement)
+                (r/rules :belief)
                 '{:statement  [--> sport competition]
                   :truth      [1 0.9]
-                  :task-type  :judgement
+                  :task-type  :belief
                   :occurrence 1000}
 
                 '{:statement  [--> chess competition]

test/nal/test/deriver/list_expansion.clj

@@ -64,11 +64,13 @@
 
 (deftest test-expand-:from-element
   (are [a1 a2] (= a1 (apply expand-:from-element a2))
-    '([--> k A1] [--> k A2] [--> k A3])
-    ['[--> k :from/A] :from/A "A" 3]
+    '(([--> k A1] :id :id-A1)
+       ([--> k A2] :id :id-A2)
+       ([--> k A3] :id :id-A3))
+    ['[[--> k :from/A] :id :id] :from/A "A" 3]
 
-    '([--> k [conj d A1]])
-    ['[--> k [conj d :from/A]] :from/A "A" 1]))
+    '(([--> k [conj d A1]] :id :id-A1))
+    ['[[--> k [conj d :from/A]] :id :id] :from/A "A" 1]))
 
 (deftest test-generate-all-lists
   (are [a1 a2] (= a1 (generate-all-lists a2))
@@ -77,58 +79,51 @@
        (W --> B)
        |-
        (W --> (| B A1))
-       :pre
-       (:question?)
-       :post
-       (:t/belief-structural-deduction :p/judgment)]
+       :pre (:question?)
+       :post (:t/belief-structural-deduction :p/judgment)
+       :id :id-A1]
        [(W --> (| B A1 A2))
         (W --> B)
         |-
         (W --> (| B A1 A2))
-        :pre
-        (:question?)
-        :post
-        (:t/belief-structural-deduction :p/judgment)]
+        :pre (:question?)
+        :post (:t/belief-structural-deduction :p/judgment)
+        :id :id-A2]
        [(W --> (| B A1 A2 A3))
         (W --> B)
         |-
         (W --> (| B A1 A2 A3))
-        :pre
-        (:question?)
-        :post
-        (:t/belief-structural-deduction :p/judgment)]
+        :pre (:question?)
+        :post (:t/belief-structural-deduction :p/judgment)
+        :id :id-A3]
        [(W --> (| B A1 A2 A3 A4))
         (W --> B)
         |-
         (W --> (| B A1 A2 A3 A4))
-        :pre
-        (:question?)
-        :post
-        (:t/belief-structural-deduction :p/judgment)]
+        :pre (:question?)
+        :post (:t/belief-structural-deduction :p/judgment)
+        :id :id-A4]
        [(W --> (| B A1 A2 A3 A4 A5))
         (W --> B)
         |-
         (W --> (| B A1 A2 A3 A4 A5))
-        :pre
-        (:question?)
-        :post
-        (:t/belief-structural-deduction :p/judgment)]
+        :pre (:question?)
+        :post (:t/belief-structural-deduction :p/judgment)
+        :id :id-A5]
        [(W --> (| B A1 A2 A3 A4 A5 A6))
         (W --> B)
         |-
         (W --> (| B A1 A2 A3 A4 A5 A6))
-        :pre
-        (:question?)
-        :post
-        (:t/belief-structural-deduction :p/judgment)]
+        :pre (:question?)
+        :post (:t/belief-structural-deduction :p/judgment)
+        :id :id-A6]
        [(W --> (| B A1 A2 A3 A4 A5 A6 A7))
         (W --> B)
         |-
         (W --> (| B A1 A2 A3 A4 A5 A6 A7))
-        :pre
-        (:question?)
-        :post
-        (:t/belief-structural-deduction :p/judgment)])
+        :pre (:question?)
+        :post (:t/belief-structural-deduction :p/judgment)
+        :id :id-A7])
     '[(W --> (| B :list/A))
       (W --> B)
       |-
@@ -136,4 +131,5 @@
       :pre
       (:question?)
       :post
-      (:t/belief-structural-deduction :p/judgment)]))
+      (:t/belief-structural-deduction :p/judgment)
+      :id :id]))

test/nal/test/deriver/rules.clj

@@ -27,7 +27,9 @@
 (def trule (rule '[(D pred-impl R) (D --> K) |- ((K pred-impl R) :post (:t/abduction)
                                                   (R --> K) :post (:t/induction)
                                                   (K </> R) :post (:t/comparison))
-                   :pre ((:!= R K))]))
+                   :pre ((:!= R K))
+                   :origin :ok
+                   :id :ok]))
 
 (deftest test-rule
   (both-equal
@@ -35,26 +37,36 @@
        :p2          (<-> S P),
        :conclusions [{:conclusion (--> S P), :post (:t/struct-int :p/judgment)}],
        :full-path   [(--> :any :any) :and (<-> :any :any)],
-       :pre         (:question?)}]
+       :pre         (:question?)
+       :origin      :ok
+       :id          :ok}]
     (rule '[(S --> P) (S <-> P) |- (S --> P) :post (:t/struct-int :p/judgment)
-            :pre (:question?)])
+            :pre (:question?)
+            :origin :ok
+            :id :ok])
 
     '({:conclusions [{:conclusion (pred-impl K R)
                       :post       (:t/abduction)}]
        :full-path   [(pred-impl :any :any) :and (--> :any :any)]
        :p1          (pred-impl D R)
        :p2          (--> D K)
-       :pre         ((:!= R K))}
+       :pre         ((:!= R K))
+       :origin      :ok
+       :id          :ok}
        {:conclusions [{:conclusion (--> R K)
                        :post       (:t/induction)}]
         :full-path   [(pred-impl :any :any) :and (--> :any :any)]
         :p1          (pred-impl D R)
         :p2          (--> D K)
-        :pre         ((:!= R K))}
+        :pre         ((:!= R K))
+        :origin      :ok
+        :id          :ok-2}
        {:conclusions [{:conclusion (</> K R)
                        :post       (:t/comparison)}]
         :full-path   [(pred-impl :any :any) :and (--> :any :any)]
         :p1          (pred-impl D R)
         :p2          (--> D K)
-        :pre         ((:!= R K))})
+        :pre         ((:!= R K))
+        :origin      :ok
+        :id          :ok-3})
     trule))

test/nal/test/deriver/terms_premutation.clj

@@ -20,27 +20,40 @@
 
 (deftest test-premure-op
   (both-equal
-    '([=|> A B] [retro-impl A B] [==> A B] [pred-impl A B])
-    (permute-op '[==> A B] implications)
+    '(([=|> A B] :id :id-perm-concur-impl)
+       ([retro-impl A B] :id :id-perm-retro-impl)
+       ([==> A B] :id :id-perm-impl)
+       ([pred-impl A B] :id :id-perm-pred-impl))
+    (permute-op '[[==> A B] :id :id] implications)
 
-    '([=|> A B] [retro-impl A B] [==> A B] [pred-impl A B])
-    (permute-op '[=|> A B] implications)
+    '(([=|> A B] :id :id-perm-concur-impl)
+       ([retro-impl A B] :id :id-perm-retro-impl)
+       ([==> A B] :id :id-perm-impl)
+       ([pred-impl A B] :id :id-perm-pred-impl))
+    (permute-op '[[=|> A B] :id :id] implications)
 
-    '(conj &| seq-conj) (permute-op '&| conjunctions)))
+    '((conj :id :id-perm-conj)
+       (&| :id :id-perm-parallel-conj)
+       (seq-conj :id :id-perm-seq-conj))
+    (permute-op '[&| :id :id] conjunctions)))
 
 (def rule1
   '{:p1          (==> M P)
     :p2          (==> S M)
     :conclusions [{:conclusion (==> S P)
                    :post       (:t/deduction :order-for-all-same :allow-backward)}]
-    :full-path   [(==> :any :any) :and (==> :any :any)]})
+    :full-path   [(==> :any :any) :and (==> :any :any)]
+    :origin      :rule1
+    :id          :rule1})
 
 (def rule2
   '{:p1          (==> M P)
     :p2          (==> S M)
     :conclusions [{:conclusion (==> S P)
                    :post       (:allow-backward)}]
-    :full-path   [(==> :any :any) :and (==> :any :any)]})
+    :full-path   [(==> :any :any) :and (==> :any :any)]
+    :origin      :rule2
+    :id          :rule2})
 
 (def rule3
   '{:p1          (==> S M)
@@ -49,137 +62,171 @@
                    :post       (:t/decompose-npp
                                  :order-for-all-same
                                  :seq-interval-from-premises)}]
-    :full-path   [(==> :any :any) :and (==> (conj :any :any) :any)]})
+    :full-path   [(==> :any :any) :and (==> (conj :any :any) :any)]
+    :origin      :rule3
+    :id          :rule3})
 
 (deftest test-order-for-all-same?
   (is ((complement nil?) (order-for-all-same? rule1)))
   (is (nil? (order-for-all-same? rule2))))
 
 (def res1
-  '({:p1          (=|> M P),
-     :p2          (=|> S M),
-     :conclusions [{:conclusion (=|> S P),
-                    :post       (:t/deduction :order-for-all-same :allow-backward)}],
-     :full-path   [(=|> :any :any) :and (=|> :any :any)],
+  '({:p1          (=|> M P)
+     :p2          (=|> S M)
+     :conclusions [{:conclusion (=|> S P)
+                    :post       (:t/deduction :order-for-all-same :allow-backward)}]
+     :full-path   [(=|> :any :any) :and (=|> :any :any)]
+     :origin      :rule1
+     :id          :rule1-perm-concur-impl
      :pre         nil}
-     {:p1          (==> M P),
-      :p2          (==> S M),
-      :conclusions [{:conclusion (==> S P),
-                     :post       (:t/deduction :order-for-all-same :allow-backward)}],
-      :full-path   [(==> :any :any) :and (==> :any :any)],
+     {:p1          (pred-impl M P)
+      :p2          (pred-impl S M)
+      :conclusions [{:conclusion (pred-impl S P)
+                     :post       (:t/deduction :order-for-all-same :allow-backward)}]
+      :full-path   [(pred-impl :any :any) :and (pred-impl :any :any)]
+      :origin      :rule1
+      :id          :rule1-perm-pred-impl
       :pre         nil}
-     {:p1          (retro-impl M P),
-      :p2          (retro-impl S M),
-      :conclusions [{:conclusion (retro-impl S P),
-                     :post       (:t/deduction :order-for-all-same :allow-backward)}],
-      :full-path   [(retro-impl :any :any) :and (retro-impl :any :any)],
+     {:p1          (retro-impl M P)
+      :p2          (retro-impl S M)
+      :conclusions [{:conclusion (retro-impl S P)
+                     :post       (:t/deduction :order-for-all-same :allow-backward)}]
+      :full-path   [(retro-impl :any :any) :and (retro-impl :any :any)]
+      :origin      :rule1
+      :id          :rule1-perm-retro-impl
       :pre         nil}
-     {:p1          (pred-impl M P),
-      :p2          (pred-impl S M),
-      :conclusions [{:conclusion (pred-impl S P),
-                     :post       (:t/deduction :order-for-all-same :allow-backward)}],
-      :full-path   [(pred-impl :any :any) :and (pred-impl :any :any)],
+     {:p1          (==> M P)
+      :p2          (==> S M)
+      :conclusions [{:conclusion (==> S P)
+                     :post       (:t/deduction :order-for-all-same :allow-backward)}]
+      :full-path   [(==> :any :any) :and (==> :any :any)]
+      :origin      :rule1
+      :id          :rule1-perm-impl
       :pre         nil}))
 
 (def res2
-  '({:p1          (pred-impl S M),
-     :p2          (pred-impl (seq-conj S :list/A) M),
-     :conclusions [{:conclusion (pred-impl (seq-conj :list/A) M),
-                    :post       (:t/decompose-npp
-                                  :order-for-all-same
-                                  :seq-interval-from-premises)}],
-     :full-path   [(pred-impl :any :any) :and (pred-impl (seq-conj :any :any) :any)],
-     :pre         nil}
-     {:p1          (retro-impl S M),
-      :p2          (retro-impl (seq-conj S :list/A) M),
-      :conclusions [{:conclusion (retro-impl (seq-conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(retro-impl :any :any)
-                    :and
-                    (retro-impl (seq-conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (=|> S M),
-      :p2          (=|> (seq-conj S :list/A) M),
-      :conclusions [{:conclusion (=|> (seq-conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(=|> :any :any) :and (=|> (seq-conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (pred-impl S M),
-      :p2          (pred-impl (conj S :list/A) M),
-      :conclusions [{:conclusion (pred-impl (conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(pred-impl :any :any) :and (pred-impl (conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (==> S M),
-      :p2          (==> (conj S :list/A) M),
-      :conclusions [{:conclusion (==> (conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(==> :any :any) :and (==> (conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (=|> S M),
-      :p2          (=|> (&| S :list/A) M),
-      :conclusions [{:conclusion (=|> (&| :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(=|> :any :any) :and (=|> (&| :any :any) :any)],
-      :pre         nil}
-     {:p1          (retro-impl S M),
-      :p2          (retro-impl (conj S :list/A) M),
-      :conclusions [{:conclusion (retro-impl (conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(retro-impl :any :any) :and (retro-impl (conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (==> S M),
-      :p2          (==> (&| S :list/A) M),
-      :conclusions [{:conclusion (==> (&| :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(==> :any :any) :and (==> (&| :any :any) :any)],
-      :pre         nil}
-     {:p1          (=|> S M),
-      :p2          (=|> (conj S :list/A) M),
-      :conclusions [{:conclusion (=|> (conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(=|> :any :any) :and (=|> (conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (pred-impl S M),
-      :p2          (pred-impl (&| S :list/A) M),
-      :conclusions [{:conclusion (pred-impl (&| :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(pred-impl :any :any) :and (pred-impl (&| :any :any) :any)],
-      :pre         nil}
-     {:p1          (==> S M),
-      :p2          (==> (seq-conj S :list/A) M),
-      :conclusions [{:conclusion (==> (seq-conj :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(==> :any :any) :and (==> (seq-conj :any :any) :any)],
-      :pre         nil}
-     {:p1          (retro-impl S M),
-      :p2          (retro-impl (&| S :list/A) M),
-      :conclusions [{:conclusion (retro-impl (&| :list/A) M),
-                     :post       (:t/decompose-npp
-                                   :order-for-all-same
-                                   :seq-interval-from-premises)}],
-      :full-path   [(retro-impl :any :any) :and (retro-impl (&| :any :any) :any)],
-      :pre         nil}))
+  '({:p1 (==> S M)
+     :p2 (==> (seq-conj S :list/A) M)
+     :conclusions [{:conclusion (==> (seq-conj :list/A) M)
+                    :post (:t/decompose-npp
+                            :order-for-all-same
+                            :seq-interval-from-premises)}]
+     :full-path [(==> :any :any) :and (==> (seq-conj :any :any) :any)]
+     :origin :rule3
+     :id :rule3-perm-seq-conj-perm-impl
+     :pre nil}
+     {:p1 (==> S M)
+      :p2 (==> (&| S :list/A) M)
+      :conclusions [{:conclusion (==> (&| :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(==> :any :any) :and (==> (&| :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-parallel-conj-perm-impl
+      :pre nil}
+     {:p1 (retro-impl S M)
+      :p2 (retro-impl (seq-conj S :list/A) M)
+      :conclusions [{:conclusion (retro-impl (seq-conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(retro-impl :any :any)
+                  :and
+                  (retro-impl (seq-conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-seq-conj-perm-retro-impl
+      :pre nil}
+     {:p1 (retro-impl S M)
+      :p2 (retro-impl (conj S :list/A) M)
+      :conclusions [{:conclusion (retro-impl (conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(retro-impl :any :any) :and (retro-impl (conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-conj-perm-retro-impl
+      :pre nil}
+     {:p1 (retro-impl S M)
+      :p2 (retro-impl (&| S :list/A) M)
+      :conclusions [{:conclusion (retro-impl (&| :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(retro-impl :any :any) :and (retro-impl (&| :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-parallel-conj-perm-retro-impl
+      :pre nil}
+     {:p1 (pred-impl S M)
+      :p2 (pred-impl (conj S :list/A) M)
+      :conclusions [{:conclusion (pred-impl (conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(pred-impl :any :any) :and (pred-impl (conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-conj-perm-pred-impl
+      :pre nil}
+     {:p1 (=|> S M)
+      :p2 (=|> (conj S :list/A) M)
+      :conclusions [{:conclusion (=|> (conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(=|> :any :any) :and (=|> (conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-conj-perm-concur-impl
+      :pre nil}
+     {:p1 (=|> S M)
+      :p2 (=|> (seq-conj S :list/A) M)
+      :conclusions [{:conclusion (=|> (seq-conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(=|> :any :any) :and (=|> (seq-conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-seq-conj-perm-concur-impl
+      :pre nil}
+     {:p1 (==> S M)
+      :p2 (==> (conj S :list/A) M)
+      :conclusions [{:conclusion (==> (conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(==> :any :any) :and (==> (conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-conj-perm-impl
+      :pre nil}
+     {:p1 (=|> S M)
+      :p2 (=|> (&| S :list/A) M)
+      :conclusions [{:conclusion (=|> (&| :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(=|> :any :any) :and (=|> (&| :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-parallel-conj-perm-concur-impl
+      :pre nil}
+     {:p1 (pred-impl S M)
+      :p2 (pred-impl (&| S :list/A) M)
+      :conclusions [{:conclusion (pred-impl (&| :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(pred-impl :any :any) :and (pred-impl (&| :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-parallel-conj-perm-pred-impl
+      :pre nil}
+     {:p1 (pred-impl S M)
+      :p2 (pred-impl (seq-conj S :list/A) M)
+      :conclusions [{:conclusion (pred-impl (seq-conj :list/A) M)
+                     :post (:t/decompose-npp
+                             :order-for-all-same
+                             :seq-interval-from-premises)}]
+      :full-path [(pred-impl :any :any) :and (pred-impl (seq-conj :any :any) :any)]
+      :origin :rule3
+      :id :rule3-perm-seq-conj-perm-pred-impl
+      :pre nil}))
 
 (deftest test-generate-all-orders
   (both-equal

test/nal/test/rules/similarity_to_inheritance.clj

@@ -0,0 +1,38 @@
+(ns nal.test.rules.similarity-to-inheritance
+  (:require [nal.rules :as r]
+            [nal.deriver.rules :refer [generate-deriver]]
+            [nal.core :refer [inference]]
+            [clojure.test :refer :all]))
+
+
+(defn get-rules [rules-name]
+  (generate-deriver (get-in r/rules [:origin rules-name])))
+
+(def rules (get-rules :similarity-to-inheritance))
+
+
+(deftest test-similarity-to-inheritance
+  (is (= '({:statement  [--> S P]
+            :task-type  :belief
+            :occurrence 1
+            :truth      [1.0 0.81]})
+         (inference rules
+                    '{:statement  [--> S P]
+                      :truth      [1 0.9]
+                      :task-type  :question
+                      :occurrence 1}
+
+                    '{:statement  [<-> S P]
+                      :truth      [1 0.9]
+                      :occurrence 0})))
+  (is (= '()
+         (inference rules
+                    '{:statement  [--> S P]
+                      :truth      [1 0.9]
+                      :task-type  :belief
+                      :occurrence 1}
+
+                    '{:statement  [<-> S P]
+                      :truth      [1 0.9]
+                      :occurrence 0}))))
+