Demey and Smessaert 2018

Demey and Smessaert compute the bitstring semantics of a finite fragment from the partition the fragment induces, without first computing its Boolean closure. In their Example 2 the fragment {p ∧ q, ¬p ∨ ¬q, p ∨ q, ¬p ∧ ¬q} of classical propositional logic has sixteen conjunctions of literals, of which three are consistent, so its closure has 2 ^ 3 elements. Their partition is Finpartition.minterms and their bitstring semantics BooleanSubalgebra.toSetOfMinterms.

Main results

• parts_minterms_example2: the three anchors of Example 2.

Implementation notes

A proposition over p and q is the finset of valuations making it true, a valuation being the pair of truth values of p and q.

References

• [DS18a]

def DemeySmessaert2018.p : Finset (Bool × Bool)

The proposition p holds at the valuations that make p true.

Equations

• DemeySmessaert2018.p = {x : Bool × Bool | x.1 = true}

def DemeySmessaert2018.q : Finset (Bool × Bool)

The proposition q holds at the valuations that make q true.

Equations

• DemeySmessaert2018.q = {x : Bool × Bool | x.2 = true}

def DemeySmessaert2018.example2 : Fin 4 → Finset (Bool × Bool)

The fragment of Example 2 is {p ∧ q, ¬p ∨ ¬q, p ∨ q, ¬p ∧ ¬q}.

Equations

• One or more equations did not get rendered due to their size.

theorem DemeySmessaert2018.parts_minterms_example2 : (Finpartition.minterms example2).parts = {p ⊓ q, (p ⊔ q) ⊓ (pᶜ ⊔ qᶜ), pᶜ ⊓ qᶜ}

The fragment of Example 2 induces the three anchors p ∧ q, (p ∨ q) ∧ (¬p ∨ ¬q) and ¬p ∧ ¬q.