CNU Logic Lab

A practice tool for Chonnam National University students studying propositional logic and predicate logic.

Generate truth tables for propositional formulas, classify them as tautologies, contradictions, or contingencies, and test argument validity.

Check whether a formula is well formed and identify its main connective. Both propositional and predicate logic are supported.

Construct a proof line by line and verify each rule application, including Fitch-style subproofs.

Expand a semantic tableau automatically to test validity or satisfiability and display a countermodel when available.

Tips

Click the on-screen logical-symbol buttons, or use the keyboard forms below.
Propositional symbols
~ or !: ¬ (negation) & or ^: ∧ (conjunction) |: ∨ (disjunction) ->: → (conditional) <->: ↔ (biconditional) \bot: ⊥ (contradiction)
Predicate-logic symbols
forall x or (x): ∀x (universal quantifier) exists x or (?x): ∃x (existential quantifier) !=: ≠ (not equal)
To avoid confusion between the term letter v and disjunction, type | or click the ∨ button.
In predicate logic, lowercase letters are treated as terms; a term is treated as a variable when bound by a quantifier and otherwise as a constant name.