Context Navigation

dcnew.ctl @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago
Add vis
File size: 681 bytes

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.