← Logic Lab

Classical propositional logic

Formal Analysis

Check validity, satisfiability, logical equivalence, and argument validity in classical propositional logic.

A formula is valid when it is true under every classical valuation.

Connectives: ¬ ∧ ∨ → ↔. Aliases: ~ & | -> <->.

Up to 10 variables across all formulas and 64 premises. Per formula: 2,048 characters, 256 nodes, and 64 levels. Constants ⊥/⊤ are not supported.

Choose an operation, fill in the fields, and click Analyze.

Local computation, without AI or storage of formulas or results.