Add Premises

Enter premises separated by commas (e.g., p, p -> q)

Proof Steps

Quick Examples

Click an example to try it:

About This Tool

This tool derives new conclusions from your premises using 10 classical propositional logic inference rules:

  • Double Negation
  • De Morgan's Laws
  • Simplification
  • Modus Ponens
  • Modus Tollens
  • Disjunctive Syllogism
  • Hypothetical Syllogism
  • Constructive Dilemma
  • Resolution
  • Adjunction

The indentation shows derivation depth. Premises sit at the left margin. Each conclusion is indented by the number of inference steps from the premises.

Supported Operators

  • ~P or not P — Negation
  • P & Q or P and Q — Conjunction
  • P | Q or P or Q — Disjunction
  • P -> Q — Implication
  • P <-> Q — Biconditional
  • P xor Q — Exclusive OR
  • P nand Q — Not AND
  • P nor Q — Not OR
  • P xnor Q — Exclusive NOR

See also

  • Truth Tables — generate truth tables for boolean expressions