search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Limitation with Simplification Rule #106

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The Simplification proof rule appears to be missing some obvious possibilities. The following illustrates:

assert:
   forall (int x, int y):
      if:
       (x <= x) || (x <= y)
      then:
       1 < 2

This produces the following proof:

 46. exists(int x, int y).((((((x + 1) >= (x + 1)) || ((y + 1) >= (x + 1)))) () 
 52. exists(int x, int y).((true || (y >= x)) && false)               (Simp 46) 
 51. (true || (y >= x)) && false                                  (Exists-E 52) 
 27. false

Observe that 52 is generated from Simp ... but why is this so weakly done? This should be further simplified.

UPDATE: It looks as though e.g. Simplification.simplifyDisjunct is pretty basic.