From 5c068c2af3b94e98c24032bb16bde733b9bdd03b Mon Sep 17 00:00:00 2001 From: konstin Date: Fri, 8 Dec 2023 14:12:04 +0100 Subject: [PATCH] Explain the rule of resolution using boolean logic --- src/internals/incompatibilities.md | 32 +++++++++++------------------- 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/src/internals/incompatibilities.md b/src/internals/incompatibilities.md index 4461742..2ac78cf 100644 --- a/src/internals/incompatibilities.md +++ b/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