Propositional Logic Proof Assistant

• Select one or more statements from the derivation sequence

• Select an inference rule from the rules panel

• Click "Apply Rule" to derive a new statement

• Continue until you derive the goal formula

• Use "Validate" to check your proof

• Note: A operation B and B operation A are not always the same. The order in which you select statements matters for some rules.

• ¬ Negation (NOT)

• ∧ Conjunction (AND)

• ∨ Disjunction (OR)

• → Implication (IF...THEN)

• ↔ Equivalence (IF AND ONLY IF)

• ⊥ Contradiction (FALSE)

• Use "New Problem" to get a different challenge

• Use "Hint" if you're stuck

• Use "Reset" to start over with current premises

• Problems are color-coded by difficulty

Goal