Operations on families of lists with extentionality

[j4n_bur53]

@kuniaki.mukai

Yes, exactly. It is after the axiom of extension of the standard set theory.

This doesn’t help you to understand classical SAT solving. In SAT solving,
and when using normal forms, like BDD, FDD, ZDD, etc… the used
equality is logical equality, which is a different thing:

• A, B: In logical equality A and B are not sets or sets of sets,
  but rather propositional formulae. This is a syntactic structure
  built from negation, conjunction, disjunction etc… and propositional variables.

• =: In logical equality equality is not extensional equality of sets or
  of sets of sets, but rather semantical or syntactical equality, whereas
  one can show that they are the same.

Currently when I input a formula in your library, and display DNF for example,
it doesn’t compute a normal form. Two different formulae A and B that are
logically equivalent can lead to different DNF in your system, i.e. Example 2:

@j4n_bur53

Example 2:

?- sat((-a)*b+a*b), psa.
 zid = 7
        [-a,b]
        [a,b]

And this here:

?- sat(b), psa.
 zid = 2
        [b]

I suspect this is just the aftermath, that your library is built upon set equality
based on extensionality, and not upon logical equality. And that you use sets
with negative and positive literals as elements. Logical equality is not so

difficult to define. It looks almost the same as set equality:

           A == B   :<=> ∀Φ(AΦ <=> BΦ)

In the above Φ is a so called valuation. A valuation is a function that sends
each propositional variable to a boolean value, i.e. Φ : Vars → Bool, where
Bool = {False, True} or if you like sometimes also expressed as Bool = {0,1}.