Worked examples: truth tables, K-maps and simplifications, step by step
Sixty worked examples, from the half adder and the majority function to eligibility rules and feature flags, each with its truth table, Karnaugh map, simplification steps, normal forms, gate forms, diagram, plain-language reading and code, all computed and verified.
The examples are the textbook canon and the rules people actually write. The canon: adders, multiplexers, comparators, parity, majority, the classic four-variable Karnaugh map, the prime-implicant example from Quine and McCluskey, the argument forms from modus ponens to the two fallacies, tautologies and contradictions, NAND-only designs. The rules: discount eligibility, access control, feature flags, loan eligibility, free shipping, an alarm, a machine interlock, a password policy, the leap-year rule, and the entry rule from the Tangibool product specification together with the slip that lets a banned member in.
Each page is generated from one seed expression by the engine and then explained by a person: what the rule means, where it is used, which step of the simplification is the one people get wrong, and which test case exposes the slip. Pages whose explanation is not yet written are generated but kept out of search indexes until it is.
Every example ends with the same rule in Python, PostgreSQL and SMT-LIB and an “Open in Tangibool” button, so you can carry it into the workspace and add your own tests.
- Entry rule: (member OR invited) AND NOT banned, checked every way
One small access rule, (member OR invited) AND NOT banned, run through every tool on the site: the eight-row truth table, the three exact checks, the simplifier, both normal forms, the NAND and NOR… - Entry rule slip: member OR (invited AND NOT banned) and the case that differs
The intended rule (member OR invited) AND NOT banned compared with the slip member OR (invited AND NOT banned). - Majority of three (2-out-of-3 voting): truth table, K-map and NAND form
Two-out-of-three voting, (A AND B) OR (A AND C) OR (B AND C): the eight-row table, a Karnaugh map with three overlapping groups, the normal forms and the 9-gate NAND construction. - Odd parity of three inputs: A XOR B XOR C
Odd parity, A XOR B XOR C, is true when an odd number of inputs are true. - Exactly one of three: why XOR is the wrong tool
The three-term formula for “exactly one of A, B, C” compared with the tempting A XOR B XOR C. - At most one of three: mutual exclusion
Mutual exclusion, NOT ((A AND B) OR (A AND C) OR (B AND C)): at most one of three inputs may be true. - Half adder sum: A XOR B
The sum bit of a half adder is A XOR B, shown next to its carry A AND B. Four rows, the XOR-elimination normal forms, a two-cell Karnaugh map and the 5-gate NAND construction. - Half adder carry: A AND B
The carry bit of a half adder is A AND B, shown next to its sum A XOR B. The simplest possible example: one true row, one-cell map, 3 gates in either family. - Full adder sum: A XOR B XOR Cin
The sum bit of a full adder, A XOR B XOR Cin, is the odd-parity function of the two operand bits and the carry-in. Eight rows, four-term normal forms, a map with four isolated ones, 20 NAND gates. - Full adder carry-out: (A AND B) OR (Cin AND (A XOR B))
The carry-out of a full adder, (A AND B) OR (Cin AND (A XOR B)), has the same truth table as majority of three. - 2-to-1 multiplexer: (S AND B) OR (NOT S AND A)
A 2-to-1 multiplexer, (S AND B) OR (NOT S AND A): the select line S picks B when true and A when false. - One-bit comparator: A greater than B
A one-bit magnitude comparator with three outputs: A AND NOT B for A greater, XNOR(A, B) for equal, NOT A AND B for B greater. The four-row table shows exactly one output true on every row. - Two-bit equality: (A1 XNOR B1) AND (A0 XNOR B0)
Two-bit equality, XNOR(A1, B1) AND XNOR(A0, B0): both bit pairs must match. Sixteen rows with four true ones, an eight-literal CNF against a sixteen-literal DNF, and a map where no two ones touch. - Seven-segment segment a from BCD with don’t-cares as assumptions
Segment a of a seven-segment display, given as the minterm list Σm(D, C, B, A; 0, 2, 3, 5, 6, 7, 8, 9) with the BCD assumption that codes 10 to 15 never occur. - BCD digit greater than five: four-variable K-map with don’t-cares
Is a BCD digit greater than five? The function Σm(D, C, B, A; 6, 7, 8, 9) under the assumption that codes 10 to 15 never occur. - Consensus in practice: AB + A'C + BC simplified
(A AND B) OR (NOT A AND C) OR (B AND C) compared with the same expression minus its third term. - Absorption in practice: A OR (A AND B) simplified
A OR (A AND B) is just A. The simplifier shows the single absorption step, the normal forms and the Karnaugh map agree, and the four-row table proves it. - De Morgan in practice: NOT (A AND B) rewritten and verified
NOT (A AND B) rewritten as NOT A OR NOT B and checked: the equivalence holds on all four rows, the normal-form converter records the De Morgan step, and the NAND-only form is a single gate. - The De Morgan slip: NOT (A AND B) vs NOT A AND NOT B
NOT (A AND B) against the slip NOT A AND NOT B. The equivalence check fails with the counterexample A = FALSE, B = TRUE, and the table marks the two rows where “not both” and “neither” disagree. - Distribution in practice: A AND (B OR C) expanded
A AND (B OR C) expanded to (A AND B) OR (A AND C) and checked on all eight rows. The factored form is already a CNF, the expanded form is the DNF, and the two gate families prefer opposite sides. - XOR built from AND, OR and NOT
A XOR B compared with (A AND NOT B) OR (NOT A AND B), the AND-OR-NOT construction of exclusive or. - XNOR built from AND, OR and NOT
XNOR(A, B) compared with (A AND B) OR (NOT A AND NOT B): equality of two bits built from the basic operators. - Implication as NOT A OR B, verified
A -> B compared with NOT A OR B: the material implication written without an arrow. - Contrapositive: A → B is equivalent to NOT B → NOT A
A -> B compared with its contrapositive NOT B -> NOT A. - The converse slip: A → B is not B → A
A -> B against its converse B -> A. The equivalence check fails with the counterexample A = FALSE, B = TRUE, and the table marks the two rows where the arrow's direction changes the answer. - The inverse slip: A → B is not NOT A → NOT B
A -> B against its inverse NOT A -> NOT B. The equivalence check fails with the counterexample A = FALSE, B = TRUE; the inverse turns out to have the same column as the converse. - Modus ponens: A → B, A, therefore B (valid)
Modus ponens: from A -> B and A, conclude B. The validity check holds on all four rows, the premises are consistent, and the table shows the single row where both premises are true. - Modus tollens: A → B, NOT B, therefore NOT A (valid)
Modus tollens: from A -> B and NOT B, conclude NOT A. The validity check holds on all four rows, with the premises jointly true only when both A and B are false. - Affirming the consequent: A → B, B, therefore A (invalid, with counterexample)
Affirming the consequent: from A -> B and B, concluding A. The validity check fails and reports the counterexample A = FALSE, B = TRUE, where both premises are true and the conclusion is false. - Denying the antecedent: A → B, NOT A, therefore NOT B (invalid)
Denying the antecedent: from A -> B and NOT A, concluding NOT B. The validity check fails with the counterexample A = FALSE, B = TRUE: the implication and the negated antecedent hold, yet B is true. - Hypothetical syllogism: A → B, B → C, therefore A → C
Hypothetical syllogism: from A -> B and B -> C, conclude A -> C. The validity check holds on all eight rows, and the premises are consistent; implications chain. - Disjunctive syllogism: A OR B, NOT A, therefore B
Disjunctive syllogism: from A OR B and NOT A, conclude B. The validity check holds on all four rows; the premises are jointly true only on A = FALSE, B = TRUE, where B is indeed true. - Constructive dilemma: (A → B) AND (C → D), A OR C, therefore B OR D
Constructive dilemma: from (A -> B) AND (C -> D) and A OR C, conclude B OR D. Four variables, a sixteen-row table, and a validity check that holds on every row. - Inconsistent premises: A and NOT A prove anything (vacuous validity)
From A and NOT A, conclude B: the validity check holds, but only vacuously, and the engine says so. The premise-consistency check is violated, which is the verdict that actually matters. - A tautology: A OR NOT A, checked on every row
A OR NOT A is true on both rows of its table. The tautology check holds, the simplifier reduces it to TRUE by the complement law, and both normal forms collapse to TRUE. - A contradiction: A AND NOT A
A AND NOT A is false on both rows of its table. The contradiction check holds, satisfiability is violated, and the simplifier reduces the formula to FALSE by the complement law. - Peirce's law: ((A → B) → A) → A is a tautology
Peirce's law, ((A -> B) -> A) -> A, is a tautology with no visible negation. - Σm(1, 2, 4, 7): canonical sum of products for three variables
A function given by its minterm list, Σm(A, B, C; 1, 2, 4, 7), expanded by the converter into four three-literal terms. - Four-variable K-map: Σm(0, 2, 5, 7, 8, 10, 13, 15) simplified
The textbook four-variable map: Σm(A, B, C, D; 0, 2, 5, 7, 8, 10, 13, 15). - Four-variable product of sums: ΠM(…) simplified from the zeros
A four-variable function given by its zeros, ΠM(A, B, C, D; 1, 3, 5, 7, 8, 10, 12, 14). - Prime implicants and essential prime implicants on a K-map
Σm(A, B, C, D; 0, 1, 2, 5, 6, 7, 8, 9, 10, 14) on a four-variable map: the engine finds six prime implicants and covers all ten ones with three of them; the cover and the derived three-term… - XOR with four NAND gates, verified equivalent
The classic four-NAND exclusive or, NAND(NAND(A, NAND(A, B)), NAND(B, NAND(A, B))), checked against A XOR B. - AND with NOR gates only
A AND B built from three NOR gates, NOR(NOR(A, A), NOR(B, B)), and checked against the plain AND. - Majority of three with NAND gates only
A hand-wired NAND circuit for majority of three, NAND(NAND(A, B), NAND(NAND(A, C), NAND(B, C))), checked against (A AND B) OR (A AND C) OR (B AND C). - Discount eligibility rule: (student OR senior) AND NOT expired AND (member OR coupon)
A five-input discount rule, (student OR senior) AND NOT expired AND (member OR coupon): a 32-row table with nine qualifying rows, a four-term DNF, 7 NOR gates against 31 NAND, and no Karnaugh map… - Feature flag rule: (beta_user OR internal) AND flag_on AND NOT kill_switch
A feature flag rule, (betauser OR internal) AND flagon AND NOT killswitch: sixteen rows with three enabling ones, a two-term DNF, two Karnaugh groups, and a NOR form of 8 gates against 23 NAND. - Access control rule: owner OR admin OR (editor AND NOT locked)
An edit-permission rule, owner OR admin OR (editor AND NOT locked): sixteen rows with thirteen permitting ones, three maxterms, a two-clause CNF, and a Karnaugh map with two eight-cell groups. - Loan eligibility: income_ok AND (credit_ok OR guarantor) AND NOT bankrupt
A loan rule, incomeok AND (creditok OR guarantor) AND NOT bankrupt: sixteen rows with three eligible ones, a two-term DNF, two Karnaugh groups, and 8 NOR gates against 23 NAND. - Free shipping rule: (over_50 OR prime) AND NOT oversized AND domestic
A shipping rule, (over50 OR prime) AND NOT oversized AND domestic: sixteen rows with three qualifying ones, a two-term DNF, and a NOR form of 7 gates against 25 NAND. - Alarm rule: armed AND (door OR window OR motion) AND NOT disarm_code
An alarm rule with five inputs, armed AND (door OR window OR motion) AND NOT disarmcode: a 32-row table with seven triggering rows, a three-term DNF, 14 NOR gates against 47 NAND, and no Karnaugh map… - Traffic-light safety property: never both greens, checked as “always true”
A safety property for a traffic light: nsgo and ewgo are each defined to exclude the other, and the formula conflict, their AND, is checked. - Machine interlock: start AND guard_closed AND NOT (estop OR fault)
A machine interlock, start AND guardclosed AND NOT (estop OR fault): of sixteen rows only one lets the machine run. - Staircase light with three switches: A XOR B XOR C
A staircase light wired to three switches, A XOR B XOR C: flipping any one switch toggles the light. - Quorum: at least three of four, truth table and K-map
A quorum of at least three out of four, written as the OR of the four triples. - Leap year rule: (div4 AND NOT div100) OR div400
The Gregorian leap-year rule, (div4 AND NOT div100) OR div400, with the arithmetic facts div400 -> div100 and div100 -> div4 stated as assumptions. - Password policy: length_ok AND (has_digit OR has_symbol) AND NOT common
A password policy, lengthok AND (hasdigit OR hassymbol) AND NOT common: sixteen rows with three accepting ones, a two-term DNF, two Karnaugh groups, and a NOR form of 8 gates against 23 NAND. - Exactly one payment option: cash, card or voucher
Exactly one of cash, card or voucher, written as three mutually exclusive terms. - Chained conditions: if premium then (discount → approved)
A nested condition, premium -> (discount -> approved): if the customer is premium, then any discount must be approved. - De Morgan in code: !(a && b) refactored to !a || !b, verified
The refactor !(a && b) to !a || !b, modelled as NOT (a AND b) against NOT a OR NOT b. - A nullable flag rule in SQL: why (a OR NOT a) is not always true
a OR NOT a is a tautology on the two-valued table, and the engine proves it. - Generated worked-example catalogue (all remaining engine examples)in progress
Questions
Can I request an example?
Yes: write to [email protected] with the rule. If it fits within the engine's limits it can be generated and explained like the others.
Why do some examples show a slice instead of a full Karnaugh map?
A Karnaugh map shows at most four variables. For a rule with more inputs the page shows the table and the normal forms, and the map tool lets you fix some inputs to view an explicitly labelled slice.
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.