Menu

#237 S /\ S is rewritten to {}

V0.9.0
closed-fixed
9
2008-11-25
2008-11-25
No

The intersection of a carrier set with itself is automatically rewritten as the empty set by the prover.

This rewriting is always wrong.

Discussion

  • Laurent Voisin

    Laurent Voisin - 2008-11-25

    This was an error in the associative commutative formula simplifier: when all expressions were cancelled, an empty set was returned instead of the type. The code is now much clearer: when the list of arguments becomes empty after simplification, return the neutral element.

    This has been fixed in CVS now and will be available in release 0.9.1.

     
  • Laurent Voisin

    Laurent Voisin - 2008-11-25
    • status: open --> closed-fixed
     

Log in to post a comment.