← Reasoning Lab
Formal Logic · Free
Proof Constructor
Build natural-deduction proofs step by step. Each inference rule is checked semantically — the validator parses your formulas and verifies the cited lines actually license the move you named, not just that you typed something in the slot.
Used in: Propositional Logic · Predicate Logic · Modal Logic · Natural Deduction lessons. Load a worked example from the dropdown to see what a complete proof looks like, or pick a practice template and try it.
Proof Constructor
Build a formal proof step by step. New here? Load a worked example from the menu below to see a complete proof, then try a practice one.
Type these symbols:
~ or ! = ¬ not& = ∧ and| = ∨ or-> = → if-then<-> = ↔ iffVariables: P, Q, R...How to use this
- Set the goal. Type the formula you want to prove into the Goal box.
- Add premises. Click + Premise for each assumption you start with. Type its formula.
- Add a derived step. Click + Derived Step. Pick the inference rule (e.g. Modus Ponens). Click the numbered buttons under Cite line(s) to mark which earlier lines this rule operates on.
- Read the live hint. Once a rule and citations are set, a hint appears showing the formula that rule would derive from those lines. Type it into the formula box.
- Click Check proof. Each derived line gets a verified / error / unchecked badge with an explanation if it failed.
Nothing here yet. The fastest way to learn this tool is to load a worked example from the menu above and read through it.
█ Premise█ Derived step