Logical equivalence checker: two expressions, exact verdict, counterexample
Check whether two Boolean expressions are logically equivalent. If they are not, the tool shows the first row where they differ, replayed through an independent evaluator.
Paste the two expressions (your version and a teammate's, a formula and its simplification, a rule before and after a refactor) and the checker asks the exact question: is there any assignment of the shared inputs on which the two differ? The engine answers by exhaustive enumeration up to twenty inputs and by a SAT solver beyond, cross-checks the result, and if a differing assignment exists it replays it through the evaluator and shows both values.
The truth table below the verdict lists both expressions as columns and highlights every differing row, so a disagreement is not a single counterexample but the complete set of cases where the two formulas disagree. For equivalent expressions the badge says on how many rows the check ran.
This is the tool behind every “with proof” label on this site: the simplifier, the normal-form converter, the gate converter and the Karnaugh map derive new forms and then call this check before showing them.
Limits
- Truth tables up to 12 inputs (4096 rows).
- Karnaugh maps up to 4 effective variables.
- Normal forms up to 4096 terms; expressions up to 20000 characters and 64 inputs.
How to write expressions
Write inputs as names (member, A, credit_ok) and combine them with AND, OR, NOT, XOR, -> (implies), <-> (if and only if), NAND(a, b), NOR(a, b), XNOR(a, b), or the symbols &&, ||, !, ∧, ∨, ¬, ·, +, ′. Minterm and maxterm forms work too: Σm(A, B, C; 1, 3), ΠM(A, B; 0). Precedence: NOT, then AND, then XOR, then OR, then ->, then <->; use parentheses to be explicit. =, ==, ^, &, | and ~ are rejected with a repair.
Example
first := NOT (A AND B) · outputsecond := NOT A AND NOT B · output
Exact checks
Truth table (4 rows)
| # | A | B | first | second |
|---|---|---|---|---|
| 0 | FALSE | FALSE | TRUE | TRUE |
| 1 | FALSE | TRUE | TRUE | FALSE |
| 2 | TRUE | FALSE | TRUE | FALSE |
| 3 | TRUE | TRUE | FALSE | FALSE |
Logic diagram
Questions
The expressions use different variable names. Can I still compare them?
Only if the names mean the same thing; the checker matches inputs by name. Rename one side so both use the same names for the same inputs, or the comparison will treat a and A as two different inputs.
Is “equivalent” the same as “equal”?
In logic, equivalent means they have the same value on every assignment, which is what is checked. = is not an operator in the engine's language; the biconditional <-> is, and A <-> B being a tautology is another way to state that A and B are equivalent.
Related
Tools
- Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns
- Boolean algebra calculator and simplifier with steps (every law named and verified)
- Karnaugh map solver: 2 to 4 variables, groups, SOP and POS, don’t-cares from assumptions
- CNF and DNF converter: conjunctive and disjunctive normal forms, minterms and maxterms
- NAND-only and NOR-only converter with equivalence proof
- Argument validity checker: premises, conclusion, counterexample or proof
- Logic circuit generator: Boolean expression to gate diagram (SVG)
- Boolean expression to Python, SQL, SMT-LIB and LaTeX
Tools
- Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns
- Boolean algebra calculator and simplifier with steps (every law named and verified)
- Karnaugh map solver: 2 to 4 variables, groups, SOP and POS, don’t-cares from assumptions
- CNF and DNF converter: conjunctive and disjunctive normal forms, minterms and maxterms
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.