Explain the rule of resolution using boolean logic

src/internals/incompatibilities.md

@@ -81,35 +81,26 @@ in the partial solution.
 
 Intuitively, we are able to deduce things such as if package \\( a \\)
 depends and package \\( b \\) which depends on package \\( c \\),
-then \\( a \\) depends on \\( c \\).
-With incompatibilities, we would note
+then \\( a \\) depends on \\( c \\). With incompatibilities, we would note
 
 \\[               \\{ a: T_a, b: \overline{T_b} \\}, \quad
                   \\{ b: T_b, c: \overline{T_c} \\}  \quad
 \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].
+This is the simplified version of the [rule of resolution][rule_of_resolution].
+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
+You can proof this implication with a truth table.
 
-\\[               \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}) \\]
+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
 
-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
-
-\\[ \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).
@@ -118,3 +109,4 @@ it can safely be replaced by the term \\( \neg [\varnothing] \\) in the expressi
 as we have already explained before.
 
 [boolean_expression]: https://en.wikipedia.org/wiki/Boolean_expression#Boolean_operators
+[rule_of_resolution]: https://en.wikipedia.org/wiki/Resolution_(logic)#Resolution_rule