Explain the rule of resolution using boolean logic

src/internals/incompatibilities.md

@@ -89,27 +89,24 @@ With incompatibilities, we would note
 \Rightarrow \quad \\{ a: T_a, c: \overline{T_c} \\}. \\]
 
 This is the simplified version of the rule of resolution.
-For the generalization, let's write them as [boolean expressions][boolean_expression].
+Let's write them as [boolean expressions][boolean_expression]:
 
-\\[               \neg (T_a \land \overline{T_b}) \quad \land \quad
-                  \neg (T_b \land \overline{T_c}) \quad
-\Rightarrow \quad \neg (T_a \land \overline{T_c}). \\]
+\\[               \overline {(T_a \land \overline{T_b})} \quad \land \quad
+                  \overline {(T_b \land \overline{T_c})} \quad
+\Rightarrow \quad \overline {(T_a \land \overline{T_c})}. \\]
 
 In fact, the above rule can also be expressed as follows
 
-\\[               \neg (T_a \land \overline{T_b}) \quad \land \quad
-                  \neg (T_b \land \overline{T_c}) \quad
-\Rightarrow \quad \neg (T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c}) \\]
+\\[               \overline {(T_a \land \overline{T_b})} \quad \land \quad
+                  \overline {(T_b \land \overline{T_c})} \quad
+\Rightarrow \quad \overline {(T_a \land (\overline{T_b \lor T_b)} \land \overline{T_c})} \\]
 
 since for any term \\( T \\), the disjunction \\( T \lor \overline{T} \\) is always true.
-In general, for any two incompatibilities \\( \\{ a: T_a^1, \cdots, z: T_z^1 \\} \\) and
-\\(  \\{ a: T_a^2, \cdots, z: T_z^2 \\}, \\)
-or
+In general, for any two incompatibilities \\( T_a^1 \land T_b^1 \land \cdots \land T_z^1 \\)
+and \\( T_a^2 \land T_b^2 \land \cdots \land T_z^2 \\) we can deduce a third,
+called the resolvent whose expression is
 
-\\[ \neg (T_a^1 \land T_b^1 \land \cdots \land T_z^1) \land  \neg (T_a^2 \land T_b^2 \land \cdots \land T_z^2), \\]
-we can deduce a third, called the resolvent whose expression is
-
-\\[ \neg ((T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2)). \\]
+\\[ (T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2). \\]
 
 In that expression, only one pair of package terms is regrouped as a union (a disjunction),
 the others are all intersected (conjunction).