1

I was quite curious about the property of wrongCommutative in PropositionalLogic example in Leon.

It seems like a correct property for me and I do not understand why it just time out in Leon.

here is the link: https://leon.epfl.ch#link/37040293ff5ff92c763f797f22f142f8-1

Can anyone help me with this?

Wenguan Huang
  • 19
  • 2

1 Answers1

2

You are right this holds, thanks for your observation! Leon did not prove it out of the box since it needs some help. It was originally wrong, but we changed the code so that the property holds for the current version of these functions.

Your "Leon stable" link seems to now point to another file (due to changes and restarts of leon.epfl.ch), but the example is still available from the list of examples on the web and here is the stable github link, to avoid any confusion.

To see why 

nnf(simplify(f)) == simplify(nnf(f))

holds for that implementation, you can observe that 

simplify(nnf(f)) = nnf(f)

as evidenced by this lemma being true:

@induct
def nnfIsSimplified(f: Formula): Boolean = {
  require(isNNF(f))
  simplify(f) == f
} holds

The fact that nnf(simplify(f))==nnf(f) can be shown by induction, but here also Leon might need some hints.

See the updated example on Github for a complete proof of this property expressed in the proof DSL of Leon.

Romain Edelmann
  • 71
  • 1
  • 3