PROOF EDITOR
Proof in logic X
⊢
p
→
q
α
1
(1)
A
α
1
(Z)
p
→
q
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
∧I
∧E
∨I
∨E
→I
→E
¬I
¬E
RAA
¬¬E
∀I
∀E
∃I
∃E
=I
=E
∀IR
∀ER
∃IR
∃ER
∀If
∀Ef
∃If
∃Ef
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
% found where a formula was expected
The error is in a formula in the URL
--- select ---
Edit line section
Restart line
Abandon current action
Help