Make terms clearer using boolean expressions

I tried to make it clear that a CDNL terms is a conjunction of negations of conjunctions by desugaring them into boolean expressions.

I'm having trouble making what's going on sufficiently clear since we need to write the negations out to apply transformation rules to them, but then they are not incompatibilities anymore but constraints that must be satisfied.

Author: konstin

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