-
Notifications
You must be signed in to change notification settings - Fork 9
/
QuantifierShift1.slt
1 lines (1 loc) · 1.53 KB
/
QuantifierShift1.slt
1
(:DESCRIPTIONS (( :X 448 :Y 873 :ID 1 :NAME "GOAL" :FORMULA "(if (and (not (exists (x) (\\phi x))) (not (forall (x) (\\phi x)))) (and (forall (x) (not (\\phi x))) (exists (x) (not (\\phi x)))))" :JUSTIFICATION LOGIC::IF-INTRO) ( :X 259 :Y 143 :ID 3 :NAME "3" :FORMULA "(\\phi x)" :JUSTIFICATION LOGIC::ASSUME) ( :X 478 :Y 260 :ID 4 :NAME "4" :FORMULA "(exists x (\\phi x))" :JUSTIFICATION LOGIC::EXISTS-INTRO) ( :X 893 :Y 120 :ID 5 :NAME "4" :FORMULA "(and (not (exists x (\\phi x))) (not (forall x (\\phi x))) )" :JUSTIFICATION LOGIC::ASSUME) ( :X 676 :Y 265 :ID 6 :NAME "6" :FORMULA "(not (exists x (\\phi x)))" :JUSTIFICATION LOGIC::AND-ELIM) ( :X 583 :Y 405 :ID 7 :NAME "7" :FORMULA "(not (\\phi x))" :JUSTIFICATION LOGIC::NOT-INTRO) ( :X 473 :Y 523 :ID 8 :NAME "8" :FORMULA "(exists x (not (\\phi x)))" :JUSTIFICATION LOGIC::EXISTS-INTRO) ( :X 676 :Y 528 :ID 9 :NAME "9" :FORMULA "(forall x (not (\\phi x)))" :JUSTIFICATION LOGIC::FORALL-INTRO) ( :X 532 :Y 735 :ID 10 :NAME "10" :FORMULA "(and (forall (x) (not (\\phi x))) (exists (x) (not (\\phi x))))" :JUSTIFICATION LOGIC::AND-INTRO)) :STRUCTURES ((:CONCLUSION 1 :PREMISES (10)) (:CONCLUSION 3 :PREMISES ()) (:CONCLUSION 4 :PREMISES (3)) (:CONCLUSION 5 :PREMISES ()) (:CONCLUSION 6 :PREMISES (5)) (:CONCLUSION 7 :PREMISES (4 6)) (:CONCLUSION 8 :PREMISES (7)) (:CONCLUSION 9 :PREMISES (7)) (:CONCLUSION 10 :PREMISES (8 9))) :INTERFACE (:X 0 :Y 0 :WIDTH 1000 :HEIGHT 800 :PROOF-SYSTEM LOGIC::FIRST-ORDER-LOGIC):CONNECTOR-TYPE "Bezier" :BACKGROUND-COLOR "white")