Assumption (domain constraint): meaning and examples

An assumption, or domain constraint, is a formula declared to hold in every admissible case of a model. Rows that violate it are excluded from the checks, and a result derived with its help is labelled as holding within the assumptions.

Assumptions capture facts about the world that the inputs alone do not express: two flags that cannot both be set, a code that never occurs, a status that implies another. They differ from premises, which are steps in an argument, and from outputs, which are what is computed. An assumption narrows the truth table to its admissible rows, so a check such as tautology asks only whether the output is true on those rows, and a Karnaugh map may treat the excluded cells as don't-cares. Contradictory assumptions leave no admissible row, and the engine marks every result vacuous.

The artefact on this page is allow = member AND NOT banned under the assumption banned -> NOT member, described as “a banned person is never a member”. The assumption column reads true on three rows and false on row 3, member = TRUE, banned = TRUE, the one excluded case. The map marks that cell don't-care and derives member, 1 prime implicant, labelled equivalent within the assumptions; the scope annotation says one cell excluded by assumption k1 was marked don't-care. The satisfiable check holds with the witness member = TRUE, banned = FALSE.

Assumptions are where business rules hide their most important facts, and where simplifications become wrong when the facts change: member is a correct rule only while banned members cannot exist. Reviewers should read a model's assumptions before its outputs. The term is confused with a premise (part of what is being argued rather than a constraint on cases), with a default value, and with an assertion in code, which is checked at run time rather than used to exclude cases.

Example

allow := member AND NOT banned · output

Assumptions: banned -> NOT member (A banned person is never a member: the membership is revoked.)

Exact checks

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

Always false (contradiction)? No Counterexample: member = T, banned = F · Exhaustively checked and solver cross-checked · 3 rows

Can be true? Yes Example assignment: member = T, banned = F · Exhaustively checked and solver cross-checked · 3 rows

Are the assumptions consistent? Yes Example assignment: member = F, banned = F · Exhaustively checked and solver cross-checked · 1 rows

Truth table (4 rows)

Assumption (domain constraint): meaning and examples
#	member	banned	allow	k1	Scope
0	FALSE	FALSE	FALSE	TRUE	in scope
1	FALSE	TRUE	FALSE	TRUE	in scope
2	TRUE	FALSE	TRUE	TRUE	in scope
3	TRUE	TRUE	FALSE	FALSE	excluded

Plain-language reading

Beginnerallow is true exactly when member is true and banned is false.
In every other case, allow is false.
About the operators:
- AND is true only when all of its parts are true.
- NOT reverses a value: true becomes false and false becomes true.

Intermediateallow is true exactly when member is true and banned is false.
In every other case, allow is false.

Advancedallow is true exactly when member is true and banned is false [conjunction ∧].
In every other case, allow is false.
Formal notation: member ∧ ¬banned

Karnaugh map

member \ banned

0m0

0m1

1m2

Xm3

cells m2, m3member

member · Derived member. The groups use don't-care cells, so the result is only claimed within the assumptions. Equivalent on every assignment the assumptions allow (scoped: it was derived using the assumptions); no claim is made outside them.

1 cell excluded by the confirmed assumptions (k1) is marked don't-care. An expression derived with them is equivalent only within the assumptions.

The common slip

Forgetting that a result derived within assumptions is only promised there. member and member AND NOT banned differ on the excluded row, and if a banned member ever appears, the simplified rule admits them. The label “equivalent within the assumptions” is the whole claim, and no claim is made outside them.

Questions

What happens if my assumptions contradict each other?

No row is admissible, so every check holds for no reason. The engine reports the scope inconsistent and marks each verdict vacuous instead of showing passes; the pitfall page on inconsistent assumptions shows that output, and the fix is to repair the assumptions.

Glossary

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.