Rev | Line | |
---|
[11] | 1 | #FAIL: fails even when weakened to AG(lamp=unlit -> EX(lamp=lit)) |
---|
| 2 | # or to AG(lamp=lit -> EX(lamp=unlit)) |
---|
| 3 | AG(((lamp = lit)->EX(lamp=unlit))*((lamp=unlit)->EX(lamp=lit))); |
---|
| 4 | #PASS: passes even when strengthened to EF(int.state=go3) |
---|
| 5 | # or to EF(int.state=go4). |
---|
| 6 | EF((int.state=go3)+(int.state=go4)); |
---|
| 7 | #PASS: no vacuous passes |
---|
| 8 | EF EG((int.state=go3)+(int.state=go4)); |
---|
| 9 | #FAIL: no vacuous failures |
---|
| 10 | !EF EG((int.state=go3)+(int.state=go4)); |
---|
| 11 | #FAIL: no vacuous failures |
---|
| 12 | AG AF(!(int.state=go3)*!(int.state=go4)); |
---|
| 13 | #FAIL: no vacuous failures |
---|
| 14 | AG((interpretation = go) -> (train = absent)); |
---|
| 15 | #PASS: passes even when strengthened to AG !(train = present2) |
---|
| 16 | AG((interpretation = go) -> !(train = present2)); |
---|
Note: See
TracBrowser
for help on using the repository browser.