Computational logic · Natural deduction
Learn natural deduction, line by line
Write proofs in Fitch notation and see every line checked, with its rule and the lines it cites.
What you can do
Prove
Enter a sequent and build the proof, with hints, an automatic solution and counterexamples.
Step by step
See a proof generated for your sequent and the strategy behind each step.
Learn
An interactive lesson on the rules, subproofs and strategies, with a quiz at the end.
Exercises
Graded proofs, with your progress saved and a “find the wrong step” mode.
What natural deduction is
It is a way of showing that a conclusion follows from some premises, one step at a time. Each line of the proof applies a simple rule to earlier lines, and a subproof lets you assume something, see where it leads and then let the assumption go.