Tableau: Contains relation in NNF

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Tableau: Contains relation in NNF
Hello,
is the formula in the attached screen correct? I would assume that the negotiation is wrong, as e.g. in the HPI lecure https://www.youtube.com/watch?v=18o0VwcowYE (at 3.38) they use don’t use the negotiation over the whole term to get a NNF form.

Attachment:
Bildschirmfoto 2020-02-03 um 20.06.19.png: https://fsi.cs.fau.de/unb-attachments/post_163282/Bildschirmfoto 2020-02-03 um 20.06.19.png

1 „Gefällt mir“

I’m not sure, but here would be some extra reasoning:

A ⊆ B means x ∈ A ⇒ x ∈ B for all x, which is the same as ¬ (x ∈ A) ∨ (x ∈ B).
If we now look at the set of all x that satisfy this, we get { x | ¬ (x ∈ A) ∨ (x ∈ B) } = complement(A) union B.
So A ⊑ B could be defined as complement(A) ⊔ B.