Update: all rules
@@ -110,12 +110,18 @@ R2( (M --> P), (M --> (S | P)), |-, (M --> S), Truth_DecomposeNPP )
R2( (M --> S), (M --> (S - P)), |-, (M --> P), Truth_DecomposePNP )
R2( (M --> S), (M --> (P - S)), |-, (M --> P), Truth_DecomposeNNN )
//NAL4 rules
-R2( ((A * B) --> R), (A --> C), |-, ((C * B) --> R), Truth_Induction )
-R2( ((A * B) --> R), (B --> C), |-, ((A * C) --> R), Truth_Induction )
R2( ((A * B) --> R), (C --> A), |-, ((C * B) --> R), Truth_Deduction )
+R2( ((A * B) --> R), (A --> C), |-, ((C * B) --> R), Truth_Induction )
+R2( ((A * B) --> R), (C <-> A), |-, ((C * B) --> R), Truth_Analogy )
R2( ((A * B) --> R), (C --> B), |-, ((A * C) --> R), Truth_Deduction )
-R2( ((A * B) --> R), (S <-> A), |-, ((S * B) --> R), Truth_Analogy )
-R2( ((A * B) --> R), (S <-> B), |-, ((A * S) --> R), Truth_Analogy )
+R2( ((A * B) --> R), (B --> C), |-, ((A * C) --> R), Truth_Induction )
+R2( ((A * B) --> R), (C <-> B), |-, ((A * C) --> R), Truth_Analogy )
+R2( (R --> (A * B)), (A --> C), |-, (R --> (C * B)), Truth_Deduction )
+R2( (R --> (A * B)), (C --> A), |-, (R --> (C * B)), Truth_Abduction )
+R2( (R --> (A * B)), (C <-> A), |-, (R --> (C * B)), Truth_Analogy )
+R2( (R --> (A * B)), (B --> C), |-, (R --> (A * C)), Truth_Deduction )
+R2( (R --> (A * B)), (C --> B), |-, (R --> (A * C)), Truth_Abduction )
+R2( (R --> (A * B)), (C <-> B), |-, (R --> (A * C)), Truth_Analogy )
//NAL5 rules
R1( (! A), |-, A, Truth_Negation )
R1( (A && B), |-, A, Truth_StructuralDeduction )
