From a18eba9bc4e3f5e2a6746f74b080fa7fe08bdd76 Mon Sep 17 00:00:00 2001 From: Jarrad Hope Date: Sun, 27 Mar 2016 16:20:57 +0200 Subject: [PATCH] cleanup part 2 --- src/nal/rules.clj | 103 +++++++++++++++++++++------------------------- 1 file changed, 48 insertions(+), 55 deletions(-) diff --git a/src/nal/rules.clj b/src/nal/rules.clj index 3685c8c..dbd54aa 100644 --- a/src/nal/rules.clj +++ b/src/nal/rules.clj @@ -18,35 +18,34 @@ ;inheritance to similarity #R[(S <-> P) (S --> P) |- (S <-> P) :post (:t/struct-abd :p/judgement) :pre (:question?)] - ;extset similarity to inheritance + ;ext-set similarity to inheritance #R[(S <-> {P}) |- (S --> {P}) :post (:t/identity :d/identity :allow-backward)] - ;intset similarity to inheritance + ;int-set similarity to inheritance #R[([S] <-> P) |- ([S] --> P) :post (:t/identity :d/identity :allow-backward)] - ;twosided extset similarity to inheritance + ;two-sided ext-set similarity to inheritance #R[({S} <-> {P}) |- ({P} --> {S}) :post (:t/identity :d/identity :allow-backward)] - ;twosided intset similarity to inheritance + ;two-sided int-set similarity to inheritance #R[([S] <-> [P]) |- ([P] --> [S]) :post (:t/identity :d/identity :allow-backward)] - ;similarity extset unwrap + ;similarity ext-set unwrap #R[({S} <-> {P}) |- (S <-> P) :post (:t/identity :d/identity :allow-backward)] - ;similarity intset unwrap + ;similarity int-set unwrap #R[([S] <-> [P]) |- (S <-> P) :post (:t/identity :d/identity :allow-backward)] ; Nothing is more specific than a instance so it's similar - ;extension of extset similar + ;extension of ext-set similar #R[(S --> {P}) |- (S <-> {P}) :post (:t/identity :d/identity :allow-backward)] ; Nothing is more general than a property so it's similar - ;intension of intset similar + ;intension of int-set similar #R[([S] --> P) |- ([S] <-> P) :post (:t/identity :d/identity :allow-backward)] - ;; Conversion, Contraposition, Negation (page 52, NAL1 NAL5) ; In term logics, "conversion" is an inference from a single premise to a conclusion by interchanging the subject @@ -66,7 +65,6 @@ ; If S can stand for P P can to a certain low degree also represent the class S ; If after S usually P happens then it might be a good guess that usually before P happens S happens. - ;conversion inheritance #R[(P --> S) (S --> P) |- (P --> S) :post (:t/conversion :p/judgement) :pre (:question?)] @@ -137,7 +135,6 @@ ; If A is a special case of B and B is a special case of C so is A a special case of C (strong) the other variations are hypotheses (weak) - ;inheritance deduction #R[(A --> B) (B --> C) |- (A --> C) :pre ((:!= A C)) :post (:t/deduction :d/strong :allow-backward)] @@ -257,28 +254,28 @@ ;; Set Comprehension: - ;predicate extset union + ;predicate ext-set union #R[(C --> A) (C --> B) |- (C --> R) :post (:t/union) :pre ((:set-ext? A) (:union A B R))] - ;predicate intset intersection + ;predicate int-set intersection #R[(C --> A) (C --> B) |- (C --> R) :post (:t/intersection) :pre ((:set-int? A) (:union A B R))] - ;subject extset intersection + ;subject ext-set intersection #R[(A --> C) (B --> C) |- (R --> C) :post (:t/intersection) :pre ((:set-ext? A) (:union A B R))] - ;subject intset union + ;subject int-set union #R[(A --> C) (B --> C) |- (R --> C) :post (:t/union) :pre ((:set-int? A) (:union A B R))] - ;predicate extset intersection + ;predicate ext-set intersection #R[(C --> A) (C --> B) |- (C --> R) :post (:t/intersection) :pre ((:set-ext? A) (:intersection A B R))] - ;predicate intset union + ;predicate int-set union #R[(C --> A) (C --> B) |- (C --> R) :post (:t/union) :pre ((:set-int? A) (:intersection A B R))] - ;subject extset union + ;subject ext-set union #R[(A --> C) (B --> C) |- (R --> C) :post (:t/union) :pre ((:set-ext? A) (:intersection A B R))] - ;subject intset intersection + ;subject int-set intersection #R[(A --> C) (B --> C) |- (R --> C) :post (:t/intersection) :pre ((:set-int? A) (:intersection A B R))] ;predicate set difference @@ -293,12 +290,15 @@ ; For example if it is known that a cat is a furry animal, it can be derived that a cat is an animal. ; So these rules are for valid deductions based on the premises containing intersections and differences. - ;; NAL3 Single Premise Inference: TODO fold this into single-premise rules? + ;; NAL3 Single Premise Inference: ; These are structural rules, that don't actually require a second premise, ; the second premise is allow us to use the two premise pattern for all rules, ; in this case it is used to confirm that a term link M exists + ; The second premise is used to only apply this rule if M actually exists and have been selected as the termlink. + ; The second premise is not used in the derivation of the conclusion as the rule is a single premise rule, it is used in control sense + ;extensional union takeout #R[((| :list/A) --> M) M |- (:from/A --> M) :post (:t/structural-deduction)] @@ -519,7 +519,7 @@ ;forward implication subject composition #R[(P =/> M) (S =/> M) |- (((P || S) =/> M) :post (:t/intersection) ((P &| S) =/> M) :post (:t/union)) - :pre ((:!= S P)) ] + :pre ((:!= S P))] ;backward implication subject composition #R[(P =\> M) (S =\> M) |- (((P || S) =\> M) :post (:t/intersection) @@ -720,7 +720,6 @@ (&& (S --> #Y) (P --> #Y)) :post (:t/intersection)) :pre ((:!= S P))] - ;variable introduction forward predicate #R[(S --> M) (P --> M) |- (((&/ (P --> $X) I) =/> (S --> $X)) :post (:t/induction :linkage-temporal) ((S --> $X) =\> (&/ (P --> $X) I)) :post (:t/abduction :linkage-temporal) @@ -728,7 +727,6 @@ (&/ (P --> #Y) I (S --> #Y)) :post (:t/intersection :linkage-temporal)) :pre ((:!= S P) (:measure-time I))] - ;variable introduction concurrent predicate #R[(S --> M) (P --> M) |- (((P --> $X) =|> (S --> $X)) :post (:t/abduction :linkage-temporal) ((S --> $X) =|> (P --> $X)) :post (:t/induction :linkage-temporal) @@ -736,14 +734,12 @@ (&| (P --> #Y) (S --> #Y)) :post (:t/intersection :linkage-temporal)) :pre ((:!= S P) (:concurrent Task Belief))] - ;variable introduction subject #R[(M --> S) (M --> P) |- ((($X --> S) ==> ($X --> P)) :post (:t/induction) (($X --> P) ==> ($X --> S)) :post (:t/abduction) (($X --> S) <=> ($X --> P)) :post (:t/comparison) (&& (#Y --> S) (#Y --> P)) :post (:t/intersection)) - :pre ((:!= S P)) ] - + :pre ((:!= S P))] ;variable introduction forward subject #R[(M --> S) (M --> P) |- (((&/ ($X --> P) I) =/> ($X --> S)) :post (:t/induction :linkage-temporal) @@ -760,7 +756,6 @@ (&| (#Y --> S) (#Y --> P)) :post (:t/intersection :linkage-temporal)) :pre ((:!= S P) (:concurrent (M --> P) (M --> S)))] - ;; Variable Syllogisms (page 57, NAL6) ; Additionally, these rules are valid due to the semantics of the dependent variables. @@ -798,10 +793,9 @@ (&& (#Y --> S) (#Y --> P) :list/A) :post (:t/intersection)) :pre ((:!= S P))] - ;second variable introduction predicate #R[(A ==> (P --> M)) (S --> M) |- (((&& A (P --> $X)) ==> (S --> $X)) :post (:t/abduction) - (&& (A ==> (P --> #Y)) (S --> #Y)) :post (:t/intersection)) ] + (&& (A ==> (P --> #Y)) (S --> #Y)) :post (:t/intersection))] ;multi variable introduction predicate #R[(&& (P --> M) :list/A) (S --> M) |- (((S --> $Y) ==> (&& (P --> $Y) :list/A)) :post (:t/abduction) @@ -843,37 +837,37 @@ ; this is what these rules are about. I am still not convinced whether these rules are really needed though. ;second-level precondition independent-var elimination - #R[(A --> K) (&& :list/B (($Y --> K) ==> (&& :list/A))) |- (&& :list/B :list/A) :pre ((:substitute $Y A)) :post (:t/deduction)] ;further generalize? + #R[(A --> K) (&& :list/B (($Y --> K) ==> (&& :list/A))) |- (&& :list/B :list/A) :pre ((:substitute $Y A)) :post (:t/deduction)] ; TODO further generalize? ;second-level postcondition dependent-var elimination #R[(A --> K) (($X --> L) ==> (&& (#Y --> K) :list/A)) |- (($X --> L) ==> (&& :list/A)) :pre ((:substitute #Y A)) :post (:t/anonymous-analogy)] ;; Temporal Inference (page 61, NAL7) TODO this is just messed up - ; Although all above rules also work for temporal statements, there are rules which are only for reasoning about time, - ; these are them. The most important one of these is temporal induction: - ; Temporal induction, a NAL7 principle, allows the system to temporally relate events. + ; Although all above rules also work for temporal statements, the following rules are only for reasoning about time. - ; The ==> and <=> Truth-related copulas are extended to capture whether two events happen after + ; The most important one of these is temporal induction, a NAL7 principle which allows the system to temporally relate events. + + ; The ==> and <=> truth-related copulas are extended to capture whether two events happen after ; each other, a =/> b, or concurrently a =|> ; These operators are all transitive, also ; ( forall a,b,c ) events with truth values ( T1, T2 in [0, 1] times [0, 1]: ) - ; a =/> b ( wedge ) b =|> c ( implies ) a =|> c with truth-value - ; induction( T1 , T2) holds, consistent with the semantics of the copulas. Additionally intervals are + ; a =/> b ( wedge ) b =|> c ( implies ) a =|> c with truth-value + ; induction( T1 , T2) holds, consistent with the semantics of the copulas. Additionally intervals are ; used to measure the temporal occurrence time difference between the events. In order to support this, ; predicate measure_time(I) is introduced which is true if and only if the the time difference between - ; both event premises is I . In the language, the time difference is encoded in the sequence, for - ; example ((&/,a,/10) =/> b) encodes that b happens 10 steps after a . + ; both event premises is I. In the language, the time difference is encoded in the sequence, for + ; example ((&/,a,/10) =/> b) encodes that b happens 10 steps after a. ;; NAL7 Specific Inference - ; Reasoning about temporal statements. those are using the ==> relation because relation in time is a relation of the truth between statements. + ; Reasoning about temporal statements. Those are using the ==> relation because relation in time is a relation of the truth between statements. ;temporal deductive detachment #R[X ((&/ K (:interval I)) ==> B) |- B :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" K X) (:shift-occurrence-forward I ==>))] #_#R[X (XI ==> B) |- B :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" XI (&/ X :interval)) (:shift-occurrence-forward XI ==>))] - ;Temporal abductive detachment + ;temporal abductive detachment #_#R[X (BI ==> Y) |- BI :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" Y X) (:shift-occurrence-backward BI ==>))] ; When P and then S happened according to an observation by induction (weak) it may be that alyways after P usually S happens. @@ -906,7 +900,6 @@ (A <-> B) :post (:p/question)) :pre (:question?)] - ;; Backward-driven Forward Inference ; For some rules it is better to only let them succeed if there is a question which explicitly asks for their result. @@ -915,31 +908,31 @@ ; NAL2: - ;similarity intset introduction + ;similarity int-set introduction #R[([A] <-> [B]) (A <-> B) |- ([A] <-> [B]) :pre (:question?) :post (:t/belief-identity :p/judgement)] - ;similarity extset introduction + ;similarity ext-set introduction #R[({A} <-> {B}) (A <-> B) |- ({A} <-> {B}) :pre (:question?) :post (:t/belief-identity :p/judgement)] - ;inheritance intset introduction + ;inheritance int-set introduction #R[([A] --> [B]) (A <-> B) |- ([A] --> [B]) :pre (:question?) :post (:t/belief-identity :p/judgement)] - ;inheritance extset introduction + ;inheritance ext-set introduction #R[({A} --> {B}) (A <-> B) |- ({A} --> {B}) :pre (:question?) :post (:t/belief-identity :p/judgement)] ; NAL3: ; Composition on both sides of a statement: - ;extensional twosided structural coposition + ;extensional two-sided structural coposition #R[((& B :list/A) --> (& A :list/A)) (B --> A) |- ((& B :list/A) --> (& A :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;intensional twosided structural composition + ;intensional two-sided structural composition #R[((| B :list/A) --> (| A :list/A)) (B --> A) |- ((| B :list/A) --> (| A :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;ext-difference twosided structural composition + ;ext-difference two-sided structural composition #R[((- S A) --> (- S B)) (B --> A) |- ((- S A) --> (- S B)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;int-difference twosided structural compositon + ;int-difference two-sided structural compositon #R[((~ S A) --> (~ S B)) (B --> A) |- ((~ S A) --> (~ S B)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] ; Composition on one side of a statement: @@ -959,22 +952,22 @@ ; NAL4: ; Composition on both sides of a statement: - ;inheritance twosided product permutation1 + ;inheritance two-sided product permutation1 #R[((* B P) --> Z) (B --> A) |- ((* B P) --> (* A P)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;inheritance twosided product permutation2 + ;inheritance two-sided product permutation2 #R[((* P B) --> Z) (B --> A) |- ((* P B) --> (* P A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;similarity twosided product permutation1 + ;similarity two-sided product permutation1 #R[((* B P) <-> Z) (B <-> A) |- ((* B P) <-> (* A P)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;similarity twosided product permutation2 + ;similarity two-sided product permutation2 #R[((* P B) <-> Z) (B <-> A) |- ((* P B) <-> (* P A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;inheritance intimage twosided introduction + ;inheritance intimage two-sided introduction #R[((\ N A _) --> Z) (N --> R) |- ((\ N A _) --> (\ R A _)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] - ;inheritance extimage twosided introduction + ;inheritance extimage two-sided introduction #R[((/ N _ B) --> Z) (S --> B) |- ((/ N _ B) --> (/ N _ S)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)] ; NAL5: