PROOF EDITOR
Proof in logic X
Symbol
Next action
Add assumption
Next proof line
Create goal
Edit goal
Delete proof line
Delete goal
Proof complete
Adding proof line ...
Edit which goal?
A
ANDI
ANDE
ORI
ORE
IMPI
IMPE
NOTI
NOTE
RAA
NOTNOTE
ALLI
ALLE
SOMEI
SOMEE
=I
=E
ALLI
R
ALLE
R
SOMEI
R
SOMEE
R
ALLI
f
ALLE
f
SOMEI
f
SOMEE
f
eK
import
export
contraction
weakening
CANCEL
Assumptions
Formula
Source lines
Rule used
Premise:
Bunching:
Conclusion:
Logic:
standard
constructive
relevant
fuzzy
linear
Quantifiers:
none
standard
restricted
free logic
Identity:
no
yes
Error message appears here.
Choose from the menu how you want to proceed:
--- select ---
Edit line section
Restart line
Abandon current action
Help