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.

Adding two one-bit numbers overflows only when both are 1, so the carry is the AND of the inputs. The model carries the sum as a second output so the table shows the full half adder: carry is true on a single row, Σm(3), where A = TRUE, B = TRUE, and sum is true on rows 1 and 2. The engine's reading is one line: carry is true exactly when both A and B are true.

The checks are as plain as the function. Tautology is violated with the counterexample A = FALSE, B = FALSE; satisfiability holds with the witness A = TRUE, B = TRUE, the one true row. The simplifier found no law that applies to a single AND. The CNF and DNF converters both return A AND B unchanged, with no law steps: two one-literal clauses, or one two-literal term. The Karnaugh map draws one group on cell 3, one prime implicant. The NAND-only form is NAND(NAND(A, B), NAND(A, B)), 3 gates, and the NOR-only form NOR(NOR(A, A), NOR(B, B)) is 3 gates as well.

This is the simplest circuit on the site, but it is the one every adder is built from: in a ripple-carry chain this carry feeds the next stage's carry-in, and the full-adder carry page shows what the next stage needs. In software, AND of two flags is a permission check or a both-conditions guard. The thing to watch is only the pairing with the sum: a carry without the sum column tells you an overflow happened but not what the low bit is.

carry := A AND B · outputsum := A XOR B · output

Exact checks

Always true (tautology)? No Counterexample: A = F, B = F · Exhaustively checked and solver cross-checked · 1 rows

Always false (contradiction)? No Counterexample: A = T, B = T · Exhaustively checked and solver cross-checked · 4 rows

Can be true? Yes Example assignment: A = T, B = T · Exhaustively checked and solver cross-checked · 4 rows

Truth table (4 rows)

Half adder carry: A AND B
#	A	B	carry	sum
0	FALSE	FALSE	FALSE	FALSE
1	FALSE	TRUE	FALSE	TRUE
2	TRUE	FALSE	FALSE	TRUE
3	TRUE	TRUE	TRUE	FALSE

Plain-language reading

Beginnercarry is true exactly when both A and B are true.
In every other case, carry is false.
About the operators:
- AND is true only when all of its parts are true.

Intermediatecarry is true exactly when both A and B are true.
In every other case, carry is false.

Advancedcarry is true exactly when both A and B are true [conjunction ∧].
In every other case, carry is false.
Formal notation: A ∧ B

Logic diagram

Simplification, step by step

The engine found no law that shortens this expression; it is already as short as its rewriting laws can make it.

A AND B

Karnaugh map

A \ B

0m0

0m1

0m2

1m3

cells m3A AND B

A AND B · Derived A AND B. Exactly equivalent on every assignment.

Minterms and maxterms

carry(A, B) = Σm(3)carry(A, B) = ΠM(0, 1, 2)

Variable order: A, B · 4 rows

Normal forms

Conjunctive normal form (CNF)

A AND B

2 clauses, 2 literals · complete

Disjunctive normal form (DNF)

A AND B

1 terms, 2 literals · complete

NAND-only and NOR-only

NAND-only form

NAND(NAND(A, B), NAND(A, B))

3 gates · verified equivalent on every row

NOR-only form

NOR(NOR(A, A), NOR(B, B))

3 gates · verified equivalent on every row

The same rule as code

Python

# -*- coding: utf-8 -*-
# Generated by Tangibool (tangibool.python/1). Do not edit by hand; regenerate from the source revision.
# Model: not stated
# Source revision: reference
# Interpretation status: not stated
"""Tangibool evaluator (decision model).

Generated deterministically from the validated Boolean model; it evaluates exactly that
model. It does not establish that the model is a complete, legal, or safe statement of a
real-world rule, and evaluating examples does not verify the rule.

Source revision: reference
Interpretation status: not stated
Exporter: 1.0.0 (format tangibool.python/1; engine 1.0.0; semantics tangibool-semantics/1)
Logic digest: f45c450824581d6decd598a105e760dcc6e773b025f7047228328714a8afd78a
Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78

Inputs (dict keys, declared order) and generated parameter names:
    'A' -> input_A
    'B' -> input_B

Outputs (declared order) and their functions:
    'carry' -> output_carry(inputs)
    'sum' -> output_sum(inputs)

Assumptions (the declared scope, checked by in_scope(inputs)):
    none; every complete assignment is in scope.

Input contract:
    Every required input must be exactly True or False (type(value) is bool). Missing
    inputs, None, strings, integers (including 0 and 1), and keys that are not declared
    inputs raise InputError before anything is evaluated, including inputs that a
    short-circuiting operator would never read. Results are always bool.

Scope:
    Decision functions raise OutOfScopeError when the inputs violate an assumption; an
    out-of-scope assignment is never turned into a False result. Pass check_scope=False
    to evaluate without the scope check, and use in_scope(inputs) to test it separately.

Usage:

    import tangibool_model as model

    model.evaluate({'A': False, 'B': False})
    # -> {'carry': False, 'sum': False}
    model.output_carry({'A': False, 'B': False})
    # -> False
    model.evaluate({'A': 1, 'B': False})
    # raises InputError: 1 is an int, not a bool
"""

import collections.abc as _abc
from typing import Dict, Mapping, Tuple

__all__ = [
    "MODEL_INFO",
    "IDENTIFIER_MAP",
    "INPUT_NAMES",
    "OUTPUT_NAMES",
    "ASSUMPTIONS",
    "InputError",
    "OutOfScopeError",
    "minterm_index",
    "in_scope",
    "evaluate",
    "output_carry",
    "output_sum",
]

MODEL_INFO = {
    "format": "tangibool.python/1",
    "mode": "decision",
    "model": None,
    "revision": "reference",
    "interpretation": None,
    "exporter": "1.0.0",
    "engine_version": "1.0.0",
    "semantics_version": "tangibool-semantics/1",
    "logic_digest": "f45c450824581d6decd598a105e760dcc6e773b025f7047228328714a8afd78a",
    "assumptions_digest": "d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78",
    "primary_output": "carry",
    "unused_inputs": (),
    "subcircuits": (),
}

# Stable ID -> generated identifier (reversible mapping; names are exact, escaped strings).
IDENTIFIER_MAP = {
    "v_4edbd11bc318": {"kind": "input", "name": "A", "identifier": "input_A"},
    "v_17a137f5e828": {"kind": "input", "name": "B", "identifier": "input_B"},
    "f_70d1fcae4401": {"kind": "output", "name": "carry", "identifier": "output_carry"},
    "f_2ac459c55f4f": {"kind": "output", "name": "sum", "identifier": "output_sum"},
}

INPUT_NAMES = ("A", "B")
OUTPUT_NAMES = ("carry", "sum")
ASSUMPTIONS = ()

_DECLARED_INPUTS = frozenset(INPUT_NAMES)
_SCOPE_INPUTS = ()
_ASSUMPTION_FORMULAS = {entry["name"]: entry["formula"] for entry in ASSUMPTIONS}


class InputError(ValueError):
    """Raised when inputs are missing, undeclared, or not exactly True/False.

    Every required input must satisfy type(value) is bool. Missing inputs, None, strings,
    integers (including 0 and 1), and keys that are not declared inputs are rejected before
    anything is evaluated. A missing input is never treated as False. The individual problems
    are listed in the problems attribute.
    """

    def __init__(self, problems):
        self.problems = tuple(problems)
        super().__init__("Invalid inputs: " + "; ".join(self.problems))


class OutOfScopeError(ValueError):
    """Raised when the inputs violate the model's assumptions (its declared scope).

    Outside its assumptions the rule has no decision: this error is never a False result.
    The names of the violated assumptions are in the violated attribute.
    """

    def __init__(self, violated):
        self.violated = tuple(violated)
        details = ", ".join(name + " (" + _ASSUMPTION_FORMULAS.get(name, "?") + ")" for name in self.violated)
        super().__init__(
            "Out of scope: the inputs violate "
            + ("assumption " if len(self.violated) == 1 else "assumptions ")
            + details
            + ". The rule has no decision outside its assumptions; this is not a False result."
        )


def _short_repr(value: object) -> str:
    text = repr(value)
    return text if len(text) <= 60 else text[:57] + "..."


def _checked_inputs(inputs: Mapping[str, bool], required: Tuple[str, ...], check_scope: bool) -> Dict[str, bool]:
    """Validate inputs strictly before anything is evaluated and return a plain copy."""
    if type(check_scope) is not bool:
        raise TypeError("check_scope must be True or False")
    if not isinstance(inputs, _abc.Mapping):
        raise InputError(["inputs must be a mapping from input names to True/False, got " + type(inputs).__name__])
    problems = []
    for key in inputs:
        if type(key) is not str or key not in _DECLARED_INPUTS:
            declared = ", ".join(repr(name) for name in INPUT_NAMES) or "none"
            problems.append("undeclared input " + _short_repr(key) + " (declared inputs: " + declared + ")")
    needed = tuple(required) + (_SCOPE_INPUTS if check_scope else ())
    for name in needed:
        if name not in inputs:
            problems.append("missing required input " + repr(name))
    for key, value in inputs.items():
        if type(key) is str and key in _DECLARED_INPUTS and type(value) is not bool:
            problems.append(
                "input " + repr(key) + " must be True or False (type bool), got "
                + type(value).__name__ + " " + _short_repr(value)
            )
    if problems:
        raise InputError(list(dict.fromkeys(problems)))
    return dict(inputs.items())


def _require_bool_args(function: str, pairs: Tuple[Tuple[str, object], ...]) -> None:
    problems = [
        "argument " + repr(name) + " of " + function + " must be True or False (type bool), got "
        + type(value).__name__ + " " + _short_repr(value)
        for name, value in pairs
        if type(value) is not bool
    ]
    if problems:
        raise InputError(problems)


def minterm_index(*values: bool) -> int:
    """Row index of an assignment over a declared variable order.

    The first value is the most significant bit, so all-False is row 0. Used for indexed
    minterm (sum) and maxterm (product) forms.
    """
    index = 0
    for value in values:
        if type(value) is not bool:
            raise InputError(["minterm_index() takes True/False values, got " + type(value).__name__ + " " + _short_repr(value)])
        index = index * 2 + (1 if value else 0)
    return index


def _scope_values(values: Dict[str, bool]) -> Tuple[Tuple[str, bool], ...]:
    """Value of every enabled, confirmed assumption for validated inputs, in declared order."""
    return ()


def _require_in_scope(values: Dict[str, bool]) -> None:
    violated = tuple(name for name, holds in _scope_values(values) if not holds)
    if violated:
        raise OutOfScopeError(violated)


def in_scope(inputs: Mapping[str, bool]) -> bool:
    """True when the inputs satisfy every assumption (the model's declared scope).

    Requires the inputs the assumptions read; raises InputError for invalid inputs.
    """
    values = _checked_inputs(inputs, (), True)
    return all(holds for _, holds in _scope_values(values))


# ---- Formula bodies (inputs are validated by the public functions below) ----


def _compute_output_carry(input_A: bool, input_B: bool) -> bool:
    """Decision output 'carry': A AND B"""
    return input_A and input_B


def _compute_output_sum(input_A: bool, input_B: bool) -> bool:
    """Decision output 'sum': A XOR B"""
    return input_A != input_B


# ---- Public API ----


def output_carry(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'carry' (stable ID f_70d1fcae4401).

    'carry' := A AND B

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_carry_value = _compute_output_carry(values["A"], values["B"])
    return output_carry_value


def output_sum(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'sum' (stable ID f_2ac459c55f4f).

    'sum' := A XOR B

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_sum_value = _compute_output_sum(values["A"], values["B"])
    return output_sum_value


def evaluate(inputs: Mapping[str, bool], *, check_scope: bool = True) -> Dict[str, bool]:
    """Evaluate every output (declared order); each output is computed once.

    Required inputs: 'A', 'B'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("A", "B"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_carry_value = _compute_output_carry(values["A"], values["B"])
    output_sum_value = _compute_output_sum(values["A"], values["B"])
    return {
        "carry": output_carry_value,
        "sum": output_sum_value,
    }

PostgreSQL

-- Tangibool PostgreSQL export (tangibool.postgresql/1)
-- Target: PostgreSQL 16 or later with typed boolean inputs; tested with PostgreSQL 18.3 (PGlite 0.5.8).
-- Not a claim of compatibility with other SQL dialects.
-- Model: not stated
-- Source revision: reference
-- Interpretation status: not stated
-- Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
-- Logic digest: f45c450824581d6decd598a105e760dcc6e773b025f7047228328714a8afd78a
-- Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
-- Mode: decision
--
-- Read-only: this file contains only WITH / VALUES / SELECT statements. No DDL, DML,
-- procedures, credentials, network access, or database changes. The expressions are pure
-- Boolean expressions, so their result does not depend on SQL evaluation order.
--
-- NON-NULL INPUT PRECONDITION: NULL is not a truth value of this rule. Every fragment below
-- is defined only when every input column it reads is a non-NULL boolean. The guard template
-- (section 2) marks any NULL input as 'invalid_input' and any row that violates the
-- assumptions as 'out_of_scope', and fills output columns only for 'ok' rows; a NULL in an
-- output column of another row is an envelope marker, not a third truth value. Never wrap
-- the fragments in COALESCE(..., FALSE) or otherwise choose a meaning for unknown inputs.
-- This evaluates the supplied model; it does not show that the model is a complete, legal,
-- or safe statement of a real-world rule.
--
-- Input columns (stable ID: name -> column):
--   v_4edbd11bc318: A -> "in_A"
--   v_17a137f5e828: B -> "in_B"
-- Output columns:
--   f_70d1fcae4401: carry -> "out_carry"
--   f_2ac459c55f4f: sum -> "out_sum"
-- Assumptions (scope K; exported separately and never folded into an output):
--   none; every complete input row is in scope.

-- ----------------------------------------------------------------------------------------------
-- 1. Expression fragments (parenthesised; non-NULL boolean inputs required)
-- ----------------------------------------------------------------------------------------------
--
-- [out_carry] output carry (stable ID f_70d1fcae4401)
--   carry := A AND B
--   PRECONDITION: "in_A", "in_B" are non-NULL booleans.
--   ("in_A" AND "in_B")
--
-- [out_sum] output sum (stable ID f_2ac459c55f4f)
--   sum := A XOR B
--   PRECONDITION: "in_A", "in_B" are non-NULL booleans.
--   ("in_A" <> "in_B")
--

-- ----------------------------------------------------------------------------------------------
-- 2. Guard template (read-only SELECT over an inputs list)
-- ----------------------------------------------------------------------------------------------
-- Replace the example rows between the markers with your own rows, or replace the inputs
-- CTE with a SELECT that provides the boolean columns listed in the header. status is
-- 'invalid_input' when any input is NULL, 'out_of_scope' when the assumptions are false, and
-- 'ok' otherwise; output columns are filled only for 'ok' rows (NULL elsewhere is an
-- envelope marker). Assumption columns are shown for rows with complete inputs.
WITH inputs ("row_id", "in_A", "in_B") AS (
  -- tangibool:example-rows:begin
  VALUES
    (1, FALSE, FALSE),
    (2, FALSE, TRUE),
    (3, TRUE, FALSE),
    (4, TRUE, TRUE),
    (5, NULL::boolean, FALSE)
  -- tangibool:example-rows:end
),
checked AS (
  SELECT
    inputs.*,
    CASE
      WHEN "in_A" IS NULL OR "in_B" IS NULL THEN 'invalid_input'
      ELSE 'ok'
    END AS "status"
  FROM inputs
)
SELECT
  "row_id",
  "in_A",
  "in_B",
  "status",
  CASE WHEN "status" = 'ok' THEN ("in_A" AND "in_B") END AS "out_carry",
  CASE WHEN "status" = 'ok' THEN ("in_A" <> "in_B") END AS "out_sum"
FROM checked
ORDER BY "row_id";

SMT-LIB

; Tangibool SMT-LIB export (tangibool.smtlib/1)
; Profile: SMT-LIB 2.6 Boolean subset (QF_UF): Bool constants, define-fun, let, push/pop, assert, check-sat, echo.
; Tested with Z3 5.1.0 (z3-solver 5.2.0, WebAssembly build).
; Model: not stated
; Source revision: reference
; Interpretation status: not stated
; Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
; Logic digest: f45c450824581d6decd598a105e760dcc6e773b025f7047228328714a8afd78a
; Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
; Mode: decision
;
; Reading results: each query block states what sat and unsat mean for its question. A sat
; answer comes with a witness or counterexample (ask for it with (get-model) after sat only);
; unsat settles that scoped query and is solver-checked, not an independently checked proof
; certificate; unknown settles nothing. Blocks are scoped with push/pop, so assertions never
; accumulate across questions. This checks the supplied model, not whether it is a complete,
; legal, or safe statement of a real-world rule.
;
; Symbols (stable ID: name -> symbol):
;   v_4edbd11bc318: A -> in_A
;   v_17a137f5e828: B -> in_B
;   f_70d1fcae4401: carry -> out_carry
;   f_2ac459c55f4f: sum -> out_sum

(set-option :produce-models true)
(set-info :smt-lib-version 2.6)
(set-logic QF_UF)

; ---- Inputs (declared order)
(declare-const in_A Bool) ; A
(declare-const in_B Bool) ; B

; ---- Outputs (dependencies first)
; output carry (stable ID f_70d1fcae4401): A AND B
(define-fun out_carry () Bool (and in_A in_B))
; output sum (stable ID f_2ac459c55f4f): A XOR B
(define-fun out_sum () Bool (xor in_A in_B))

; ---- Assumptions (the scope K; never folded into an output)
; K: conjunction of the enabled, confirmed assumptions (true when there are none)
(define-fun K () Bool true)

; ---- Definitions only: nothing is asserted and no check is run.
; Add (assert ...) and (check-sat) inside (push 1) ... (pop 1) to ask a question.

LaTeX

carry = A \cdot B
sum = A \oplus B

The common slip

Expecting a NAND circuit for AND to be a single gate. A NAND gate is an AND followed by an inverter, so the converter needs a second NAND wired as an inverter to undo it: 3 gates, not 1. The table proves the two-gate chain returns to A AND B.

Questions

Why does the CNF say two clauses for A AND B?

In conjunctive normal form every clause is an OR of literals, and a single literal counts as a clause. A AND B is the conjunction of the clauses A and B, so the converter reports two clauses and two literals, with no rewriting needed.

Guides

Half adder and full adder

Operators and gates

Tools

Worked examples

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. 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.

Half adder carry: A AND B

Exact checks

Truth table (4 rows)

Plain-language reading

Logic diagram

Simplification, step by step

Karnaugh map

Minterms and maxterms

Normal forms

Conjunctive normal form (CNF)

Disjunctive normal form (DNF)

NAND-only and NOR-only

NAND-only form

NOR-only form

The same rule as code

The common slip

Questions

Related

Guides

Operators and gates

Tools

See also

Worked examples