Explain the rule of resolution using boolean logic

[konstin]

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

[mpizenberg]

The notation is introduced in the previous page: https://pubgrub-rs-guide.netlify.app/internals/terms#definition

[konstin]

I've moved the rust translation over to terms#definition. I think explicitly stating the $\neg A$ is the same as $\overline{A}$ will be easier to follow for most programmers.

[mpizenberg]

Remark that I took the symbol "¬" from the literature, https://en.wikipedia.org/wiki/Literal_(mathematical_logic).
In general, that symbol corresponds to a proposition. Something like "x is inside set A", or "x is not inside set A". On the other hand the hat is the complement operator on sets, and not something that operates on propositions.

So I've been abusing a bit the notation. Because saying "x is not inside set A" is linked to saying "x is inside the complement of A". But maybe I should not have mixed the two notations. I'm not sure what is the most correct way to say all of this.

[mpizenberg]

I think "¬" should not appear except for literal definition.
Now that I re-read what I wrote, it is correct. I did not use "¬" for anything else than literals and what you propose is not correct.

[konstin]

I have to admit that i only got the mathematics-for-computer-scientist version, where $\overline{A}$ was treated as a convenience for $\neg A$. I'll definitely remove the part if it's not correct for the kind of logic we're using.

[mpizenberg]

Yeah it's not correct to use that symbol when dealing with the terms, and not at the literal level. However, if it isn't clear enough for the programming side of the brain, we might need to make it clearer indeed.

[konstin]

I've split the PRs, this is now only about using the full boolean expression

[mpizenberg]

Actually, I might have got it backwards. While forcing set notation on terms, which intrinsically are propositions. So maybe it should be "¬" all the way. And complements should never appear, except when explaining the equivalence between terms and ranges sets, and how we use that equivalence to evaluate terms intersection (conjunction).
Sorry about that.

[konstin]

I'd like to re-up this for review, i've moved the contentious part to #9, this PR itself should be easy to merge.

[mpizenberg]

Right sorry forgot about this. I remember wanting to change a thing. I'll be back on sunday and can provide more context for what I had in mind then.

[konstin]

I've updated the explanation and added a reference, i hope i didn't mix up the symbols again