Abstract Logic

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

Examples: (p implies q), (p and (not q)), (p or (not p))

Abstract Proof Engine

Put one premise per line, then add a goal.

Tableau: Basic extraction order. V2: Prioritizes Alpha (non-branching) rules. V3: Evaluates all premise permutations to find the optimal tree. V4: Prioritizes Beta formulas with the lowest OR count in their CNF form.

Abstract Formula Evaluation

Abstract Truth Table

Check tautology, contradiction, or contingency.