How to write expressions

Variables are names that start with a letter: A, p, rain, x1. Several spellings are accepted for each operator, so you can paste formulas from most textbooks and programming languages.

Operator	Type any of	Binds
not	`not A`, `!A`, `~A`, `¬A`, `A'`	tightest
and, nand	`and`, `&`, `&&`, `*`, `·`, `∧`; `nand`, `↑`
xor	`xor`, `^`, `⊕`
or, nor	`or`, `\|`, `\|\|`, `+`, `∨`; `nor`, `↓`
implies	`->`, `=>`, `→`, `implies`	groups to the right
if and only if	`<->`, `<=>`, `==`, `↔`, `iff`	loosest
constants	`0`, `1`, `true`, `false`, `⊤`, `⊥`

So A or B and not C means $A \lor (B \land \lnot C)$ , and A -> B -> C means $A \to (B \to C)$ , the usual convention in logic. When in doubt, add parentheses; the generator prints back the expression it understood, with only the parentheses that are needed.

What the output means

Rows are listed in binary counting order, the first variable being the most significant bit, so row $i$ is the assignment whose bits spell $i$ . Tick “Start with 1s” for textbooks that put T first.
Sub-expression columns show each intermediate result, innermost first, so you can check a hand-written table column by column. The last column is the whole expression.
Canonical DNF is the OR of one minterm per row where the expression is 1, written $\Sigma m(\dots)$ with the row numbers. Canonical CNF is the AND of one maxterm per row where it is 0, written $\Pi M(\dots)$ .
Minimal DNF and CNF use as few terms as possible, then as few literals as possible. They are computed with the Quine–McCluskey method and an exact search over prime implicants.

Worked example: $(A \to B) \land (B \to C) \to (A \to C)$

This is the rule that implication chains: if A implies B and B implies C, then A implies C. It has 3 variables and 8 rows. The final column is 1 in every row, so it is a tautology: valid whatever A, B and C are. Its canonical DNF lists all eight minterms, its canonical CNF is empty (written 1), and both minimal forms are simply 1.

Using the LaTeX output

The table output is a plain tabular with a vertical rule between the variables and the computed columns, using only standard LaTeX, so it compiles in any document class. Formulas use \land, \lor, \lnot, \oplus, \rightarrow and \leftrightarrow. If your venue prefers \wedge and \vee, they are the same symbols. For a typeset table with nicer rules, load booktabs and replace \hline with \midrule; see the LaTeX templates guide.

Checking equivalence

Two expressions are equivalent when they agree on every assignment. Open “Check whether two expressions are equivalent” under the table to compare two formulas. When they differ, you get a specific counterexample, which is usually the fastest way to find a mistake in a simplification.

Limits The table is limited to 8 variables (256 rows) so that it stays readable, and the equivalence check to 12 variables. Beyond that, exhaustive tables are the wrong tool: a SAT solver can decide satisfiability and equivalence of much larger formulas.

Learn the background

The Boolean algebra explainer covers the laws, normal forms and functional completeness behind this tool, with worked examples.

Truth table generator