Skip to content

Lesson 13: Categories, scales, and counting (intermediate, 20 min)

Rules say “the plan is one of these”, “rated BBB- or better” and “at least two of three criteria”. This lesson models each with a category input, an ordered scale and a counting constraint, and shows how the engine derives the facts that relate the tests. Four steps, intermediate level, about twenty minutes.

Level: intermediate20 min10 claims in this lesson were confirmed by the exact checker at build time

Model “the plan is one of these”, “rated BBB- or better”, and “at least two of three” with category inputs, ordered scales, and counting constraints, and see how the engine derives the facts that relate them.

The first step gives the plan one value, Free, Basic, Pro or Team, rather than four independent TRUE/FALSE inputs. Formulas test it with lists, plan IN Paid and plan IN Collaborative, and each test is a TRUE/FALSE input the engine derives from the value, so a scenario can give the plan itself. The second step shows what the lists imply: every collaborative plan is paid, so the engine derives the assumption plan IN Collaborative -> plan IN Paid and applies it in every check and table. The four plans fall into three classes that every test treats alike, and the truth table over the two tests and invited_by_team has six admissible rows, not eight.

The third step orders the levels of a credit-rating scale and defines rating_at_least_BBB_minus as “BBB- or better”, which rating ≥ A implies. Not rated is an outside value, on no level and satisfying no comparison, which is why NOT rating_at_least_BBB_minus and rating_below_BBB_minus differ: the lesson’s claim that the two outputs are not equivalent is verified at build time, and the witness is the unrated bond. The fourth step writes “at least two of three criteria” as AT_LEAST(2; …), one gate that counts, and checks it equivalent to the majority formula and not equivalent to the XOR chain, which is parity.

The exercises ask what a Pro customer can do without an invitation, for the rating situation where the two negative outputs differ, and for the majority written with AND and OR only. The worked examples on majority, quorum and exactly-one show the expanded forms that the counting-constraint expansion law produces, and the pitfall page on XOR chains shows the row where parity and “exactly one” part company.

Do this lesson interactively in the app

Steps

1. A category input takes one value

The plan is Free, Basic, Pro, or Team: one value, not four independent TRUE/FALSE inputs. Formulas test the value with lists: plan IN Paid is TRUE for Basic, Pro, and Team; plan IN Collaborative for Pro and Team.

Each test is a TRUE/FALSE input the engine derives from the value, so a scenario can give the plan itself, and every test follows.

can_share := plan IN Collaborative OR (plan IN Paid AND invited_by_team) · output

plan: the customer’s plan; invited_by_team: a team member invited the customer; can_share: the customer may share the document;

A category input takes one value
#plan_in_Collaborativeplan_in_Paidinvited_by_teamcan_shareplan_values_1Scope
0FALSEFALSEFALSEFALSETRUEin scope
1FALSEFALSETRUEFALSETRUEin scope
2FALSETRUEFALSEFALSETRUEin scope
3FALSETRUETRUETRUETRUEin scope
4TRUEFALSEFALSETRUEFALSEexcluded
5TRUEFALSETRUETRUEFALSEexcluded
6TRUETRUEFALSETRUETRUEin scope
7TRUETRUETRUETRUETRUEin scope

Set the plan to Basic with invited_by_team FALSE and watch both tests and the output.

2. Derived facts: a collaborative plan is paid

Every value in Collaborative is also in Paid, so no plan makes plan IN Collaborative TRUE and plan IN Paid FALSE. The engine derives the assumption plan IN Collaborative -> plan IN Paid from the lists and applies it everywhere: checks, truth tables, and tests never consider that impossible combination.

The four plans fall into three classes that every test treats alike: Free; Basic; Pro and Team. A truth table over the two tests and invited_by_team has six admissible rows, not eight.

can_share := plan IN Collaborative OR (plan IN Paid AND invited_by_team) · output

plan: the customer’s plan; invited_by_team: a team member invited the customer; can_share: the customer may share the document;

Derived facts: a collaborative plan is paid
#plan_in_Collaborativeplan_in_Paidinvited_by_teamcan_shareplan_values_1Scope
0FALSEFALSEFALSEFALSETRUEin scope
1FALSEFALSETRUEFALSETRUEin scope
2FALSETRUEFALSEFALSETRUEin scope
3FALSETRUETRUETRUETRUEin scope
4TRUEFALSEFALSETRUEFALSEexcluded
5TRUEFALSETRUETRUEFALSEexcluded
6TRUETRUEFALSETRUETRUEin scope
7TRUETRUETRUETRUETRUEin scope

Open the truth table and count the rows; then open the assumptions and find the derived one.

contingent can_share · holds

3. Scales: “BBB- or better” and the outside value

A scale orders its levels from lowest to highest, so rating_at_least_BBB_minus means “BBB- or better” and the engine knows that rating ≥ A implies it. Not rated is an outside value: it is on no level and satisfies no comparison.

That is why NOT rating_at_least_BBB_minus and rating_below_BBB_minus differ: a bond that is not rated makes the first TRUE and the second FALSE. The editor warns where NOT applies to such a threshold; say what you mean with the explicit test.

investment_grade := rating_at_least_BBB_minus · outputnot_investment_grade := NOT rating_at_least_BBB_minus · outputspeculative := rating_below_BBB_minus · output

rating: the agency’s rating of the bond; investment_grade: the bond is investment grade; not_investment_grade: the bond is not investment grade (including when it is not rated); speculative: the bond is rated below BBB-;

Scales: “BBB- or better” and the outside value
#rating_at_least_BBB_minusrating_below_BBB_minusinvestment_gradenot_investment_gradespeculativerating_order_1Scope
0FALSEFALSEFALSETRUEFALSETRUEin scope
1FALSETRUEFALSETRUETRUETRUEin scope
2TRUEFALSETRUEFALSEFALSETRUEin scope
3TRUETRUETRUEFALSETRUEFALSEexcluded

Set the rating to Not_rated and compare not_investment_grade with speculative.

not-equivalent not_investment_grade / speculative · holds

4. “At least two of three” is a count, not a chain of XOR

AT_LEAST(2; a, b, c) counts how many operands are TRUE and compares the count with 2. EXACTLY(2; …) and AT_MOST(2; …) work the same way. A chain a XOR b XOR c is parity: TRUE when one or all three are TRUE, which is rarely what a rule means.

EXACTLY(1; a, b, c) is how to write “exactly one”. It differs from the XOR chain exactly when all three are TRUE.

meets_test := AT_LEAST(2; trades_at_least_10, portfolio_over_500000, finance_role_at_least_1_year) · outputexactly_two := EXACTLY(2; trades_at_least_10, portfolio_over_500000, finance_role_at_least_1_year) · outputparity := trades_at_least_10 XOR portfolio_over_500000 XOR finance_role_at_least_1_year · outputmajority := (trades_at_least_10 AND portfolio_over_500000) OR (trades_at_least_10 AND finance_role_at_least_1_year) OR (portfolio_over_500000 AND finance_role_at_least_1_year) · output

trades_at_least_10: at least 10 significant trades a quarter; portfolio_over_500000: a portfolio over 500,000 euros; finance_role_at_least_1_year: at least a year in a relevant finance role; meets_test: the client meets the quantitative test (two of three); exactly_two: exactly two criteria are met; parity: an odd number of criteria are met (a chain of XOR); majority: the same test written with AND and OR only;

“At least two of three” is a count, not a chain of XOR
#trades_at_least_10portfolio_over_500000finance_role_at_least_1_yearmeets_testexactly_twoparitymajority
0FALSEFALSEFALSEFALSEFALSEFALSEFALSE
1FALSEFALSETRUEFALSEFALSETRUEFALSE
2FALSETRUEFALSEFALSEFALSETRUEFALSE
3FALSETRUETRUETRUETRUEFALSETRUE
4TRUEFALSEFALSEFALSEFALSETRUEFALSE
5TRUEFALSETRUETRUETRUEFALSETRUE
6TRUETRUEFALSETRUETRUEFALSETRUE
7TRUETRUETRUETRUEFALSETRUETRUE

Make all three criteria TRUE and compare meets_test, exactly_two, and parity.

not-equivalent meets_test / parity · holdsequivalent meets_test / majority · holds

Exercises

  1. The plan is Pro (so plan IN Paid and plan IN Collaborative are both TRUE) and nobody invited the customer. Can the customer share? (predict-output)
  2. Find the rating situation where not_investment_grade and speculative differ (hint: it is not on any level). (find-assignment)
  3. Write meets_test (“at least two of the three criteria”) with AND and OR only, without a counting constraint. (write-equivalent)

Do this lesson interactively in the app

Questions

What is a value class?

A set of values that every test the logic uses treats alike. With the lists Paid and Collaborative, Free is one class, Basic another, and Pro and Team a third, because no test tells them apart. Checks, truth tables and coverage work on classes, so a category with hundreds of values stays small.

Why is NOT rating_at_least_BBB_minus not the same as rating_below_BBB_minus?

Because an outside value such as Not rated fails every comparison on the scale. An unrated bond makes the first TRUE and the second FALSE, and the editor warns where NOT is applied to a scale threshold so you can say which one you mean.

Related

Tools

See also

Lessons

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.