diff --git a/src/internals/incompatibilities.md b/src/internals/incompatibilities.md index 5a83a8a..4461742 100644 --- a/src/internals/incompatibilities.md +++ b/src/internals/incompatibilities.md @@ -89,28 +89,32 @@ 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 reuse the "more mathematical" notation of conjunctions -for incompatibilities \\( T_a \land T_b \\) and the above rule would be +For the generalization, let's write them as [boolean expressions][boolean_expression]. -\\[ T_a \land \overline{T_b}, \quad - T_b \land \overline{T_c} \quad -\Rightarrow \quad T_a \land \overline{T_c}. \\] +\\[ \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}). \\] In fact, the above rule can also be expressed as follows -\\[ T_a \land \overline{T_b}, \quad - T_b \land \overline{T_c} \quad -\Rightarrow \quad T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c} \\] +\\[ \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}) \\] since for any term \\( T \\), the disjunction \\( T \lor \overline{T} \\) is always true. -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 +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 -\\[ (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). \\] +\\[ \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)). \\] In that expression, only one pair of package terms is regrouped as a union (a disjunction), the others are all intersected (conjunction). If a term for a package does not exist in one incompatibility, it can safely be replaced by the term \\( \neg [\varnothing] \\) in the expression above as we have already explained before. + +[boolean_expression]: https://en.wikipedia.org/wiki/Boolean_expression#Boolean_operators