Natural Deduction Proof Checker
Sentential Logic
Problem Gen 1 →
Problem Gen 2 →
New Proof
~
·
∨
⊃
≡
(
)
Premises
+ Add another premise
Conclusion
Begin Proof →
Tip:
Click an operator button above, or type shortcuts:
->
for ⊃
&
or
*
for ·
v
for ∨
<->
for ≡. Lowercase atomic letters are automatically capitalized. Parentheses are required around each embedded connective: write
A ⊃ (B · C)
, not
A ⊃ B · C
.
New Proof
✓ Proof complete!
Line
Formula
Justification
Status
~
·
∨
⊃
≡
(
)
Keyboard shortcuts:
->
→ ⊃
&
/
*
→ ·
v
→ ∨
<->
→ ≡
[ ]
→ ( )
Formula for the next proof line
Rule
— select —
MP — Modus Ponens
MT — Modus Tollens
HS — Hypothetical Syllogism
DS — Disjunctive Syllogism
Simp — Simplification
Conj — Conjunction
Add — Addition
CD — Constructive Dilemma
DM — De Morgan
Com — Commutation
Assoc — Association
Dist — Distribution
DN — Double Negation
Trans — Transposition
Impl — Material Implication
Equiv — Material Equivalence
Exp — Exportation
Taut — Tautology
Lines
Add Line
Open CP
Open IP
Close Subproof
Undo
Reset