Add Premises

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

Proof Steps

Quick Examples

Click an example to load its premises and explore different inference rules:

About This Tool

This logic proof engine automatically 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 are at the left margin, and conclusions are indented based on how many inference steps they are 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

Navigation