Abstract Logic

Formal symbolic logic workspace. The applied proposition composer is on its own page.

Prop examples: (p implies q), (p and (not q)) | Predicate examples: forall x. (P(x) -> Q(x)), exists y. R(y)

Open Applied Logic Page Sample Problems ↓ Predicate Logic

Abstract Proof Engine

Put one premise per line, then add a goal.

Premises Goal

Abstract Formula Evaluation

Formula Assignments (JSON)

Abstract Truth Table

Check tautology, contradiction, or contingency.

Formula

Predicate Logic Tableau

First-order logic with ∀/∃ quantifiers. Syntax: forall x. P(x), exists y. R(x, y), P(a). Bound identifiers are variables; unbound ones are constants.

Premises (one per line) Goal Max gamma rounds