status-im/narjure
2
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

cleanup part 2

Browse Source
This commit is contained in:
Jarrad Hope
2016-03-27 16:20:57 +02:00
parent a7cf3d9433
commit a18eba9bc4
1 changed files with 48 additions and 55 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/nal/rules.clj
+48 -55
View File
@@ -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: