# Strict rules

**In one sentence:** `rule … strict` is inference without exceptions: once the
body is established, the head gains positive support that no defeater, no
priority, and no `unless` can remove. The author uses it when the norm holds
always within its scope of applicability, and the applicability conditions lie
entirely in the body.

The language specification treats a strict rule as inference without
exceptions: once the body is established, the head gains support that no
defeater and no priority can remove. The defeasible forms live on the
[defeasible rules page](/constructs/rule-defeasible-unless/).

## 1. When to use and when not to

| Instead | Selection rule |
|---|---|
| `strict` vs `defeasible` | Exceptions possible even in principle — `defeasible`. `strict` only when the opposite conclusion on the same premises is impossible by the substance of the norm, not “until someone invents an exception”. Check: if an `unless` is needed later, the rule must be rewritten with a change of strength, because `unless` on `strict` is a rejection `LDC-E4110` |
| `strict` vs `definition … exact` | Qualification of a concept with a name (“who counts as …”) — `definition`: generated nodes carry the `was_derived_from` edge, and the explanation says “by definition”. Inferring a fact from facts without naming a concept — `rule strict`. The observed status is the same for both forms; the difference is in the proof graph |
| `strict` with head `not p(x)` vs defeater `defeat p(x)` | An explicit refusal (“prohibited”, “not allowed”) is needed — a strict negative head: gives Refuted. “Remove the permission, asserting nothing” is needed — a defeater: gives Not established, not refuted. Confusing them is an error: after a defeater the question stays open, after a negative head it is closed by refusal |
| Two strict rules with opposite heads vs a `defeasible` + `priority` pair | A conflict of two `strict` rules is preserved as Contradiction forever: priority is powerless here. A resolvable conflict is `defeasible` + `priority` (see the [priority page](/constructs/priority/)) |

## 2. Minimal example

Package `research.rule_strict.strict_guard`: a small enterprise — up to 100 employees
inclusive. Vocabulary — one entity and two relations; the guard `n <= 100` is
a body conjunct, and the literal `employee_count(e, n)` binds the variable
`n` (comparing variables does not bind).

```law
entity Enterprise {
    label ru-KZ official "Предприятие";
}
relation employee_count(e: Enterprise, n: Integer) kind empirical {
    label ru-KZ official "численность работников";
}
relation small_enterprise(e: Enterprise) kind institutional {
    label ru-KZ official "является малым предприятием";
}
rule SmallEnterprise strict {
    label ru-KZ official "Малое предприятие: до 100 работников включительно";
    for e: Enterprise;
    for n: Integer;
    when employee_count(e, n) and n <= 100;
    then small_enterprise(e);
}
```

Case facts: `employee_count(urn:case:research:strict:alpha, 80)` with
`origin case_input`. Query: `evaluate truth(small_enterprise(...))`.

Actual engine answer:

```text
law test research.rule_strict.strict_guard: мир research.rule_strict.strict_guard
  ok   [research.rule_strict.strict_guard#authored] tests/01-small-enterprise.lawtest / urn:query:research-strict-01
  ok   [research.rule_strict.strict_guard#authored] tests/02-large-enterprise.lawtest / urn:query:research-strict-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings. Sensitivity:
a case with `employee_count(…, 250)` gives Not established, not refuted
(the large-enterprise test): the rule stays silent, it does not
refuse — only explicit negations give negative support. Removing the
`employee_count` fact also gives Not established, not refuted — the example is not vacuous.

Second package `research.rule_strict.strict_conflict`: two strict rules with
opposite heads:

```law
rule RegisteredMayTrade strict {
    for v: Trader;
    when registered_trader(v);
    then may_trade(v);
}
rule ProhibitedGoodsBan strict {
    for v: Trader;
    when sells_prohibited_goods(v);
    then not may_trade(v);
}
```

Actual answer: both facts — Contradiction (the conflict test),
only `registered_trader` — Established
(the single-support test), `law test` — 2/2. Sensitivity:
removing the `sells_prohibited_goods` fact changes Contradiction to Established.
No `priority` can resolve this conflict — see the
[strict-rule pitfalls](/constructs/rule-strict/pitfalls/),
item 5.

Note on head forms: a strict negative head `then not may_trade(v)`
is explicit negative support, not negation-as-failure. Without
the `sells_prohibited_goods` fact the rule yields nothing — neither
Refuted nor Not established, not refuted with an issue: it simply does not apply. That is
why the pair “permission by strict rule + prohibition by strict rule” on an
empty case answers Not established, not refuted on both premises, not “permitted until
prohibited”: permission is derived only by the established body
`registered_trader(v)`.

## 3. Example by domain

- **Law:** package `kz.corpus.civilcode` (Civil Code of Kazakhstan) —
  a strict rule with header parameters: qualification of a person as a natural person.
- **Law:** package `kz.corpus.civilcode` (Civil Code of Kazakhstan), liquidation —
  a defeasible norm next to strict ones: distribution of property
  on insufficiency — `defeasible`, because the statute admits “unless otherwise provided”.
- **International law:** package `intl.ihl.geneva_1949` (Geneva Convention III of 1949) —
  a defeater as a neighbour of the strict form: removal of a status without
  asserting the opposite.
- **Teaching case:** package `research.rule_strict.strict_conflict` — a preserved Contradiction
  conflict in miniature: the same mechanics as a collision of two imperative
  norms of one level.

## 4. How the engine answers

Table — actual runs of this section’s teaching packages:

| Facts | Question | Answer | Why |
|---|---|---|---|
| `employee_count(alpha, 80)` | `small_enterprise(alpha)` | Established | body established, strict support |
| `employee_count(beta, 250)` | `small_enterprise(beta)` | Not established, not refuted | guard not met; rule silent |
| no facts | `small_enterprise` | Not established, not refuted | no rule fired — and that is not a refusal |
| `registered_trader`, `sells_prohibited_goods` | `may_trade` | Contradiction | two strict opposite supports preserved |
| only `registered_trader` | `may_trade` | Established | second premise absent |
| `registered` | `taxpayer` | Established | first head of the registration-effects block |
| `registered` | `may_open_bank_account` | Established | second head of the same block |

- A bare body literal reads as established: a fact in Contradiction
  does not activate a strict rule.
- In `proof`, every application is addressable by its identity (rule id +
  substitution + input hash + activation key).
- In `why_not`, an unfired strict rule names the unestablished
  conjunct; strict support takes no part in another’s defeat explanation —
  nobody defeats it.
- Scenarios of the small-enterprise test: given
  `assert employee_count(entity_ref("urn:tutorial:alpha"), 80)` →
  `evaluate truth(small_enterprise(...))` → Established;
  given `employee_count(entity_ref("urn:tutorial:beta"), 250)` → the same
  query → Not established, not refuted — these are rows 1–2 of the table above.

## 5. Common mistakes

1. Guard instead of a binding literal (`when n <= 100` without
   `employee_count(e, n)`) — `LDC-E4101` (pitfalls, item 1).
2. `unless` on a strict rule — `LDC-E4110` (pitfalls, item 2).
3. Defeater against a strictly produced head — `LDC-E4112`
   (pitfalls, item 3).
4. Expecting Refuted where the rule simply did not fire —
   Not established, not refuted without negative support (pitfalls, item 4).
5. `priority` over a strict rule (`LDC-E4105`) and hoping to resolve
   a conflict of two `strict` rules by priority (pitfalls, item 5).
6. A separate `relation` for a `definition` name — `LDC-E1201`
   (pitfalls, item 6).

## 6. References

- Neighbour pages: [defeasible rules](/constructs/rule-defeasible-unless/)
  (defeasible rules, `unless`, defeater), [negation](/constructs/negation-and-status/)
  (negation), [priority](/constructs/priority/) (conflict and priority).
- The pitfalls page lists the diagnostics (`LDC-E4101`, `LDC-E4110`,
  `LDC-E4112`, `LDC-E4105`, `LDC-E1201`) with wrong forms and fixes.

## 7. Grammar excerpt

Productions of the `rule_decl` family (`strict` strength is one alternative
of `rule_strength`; defeat and priority live on the
[defeasible rules](/constructs/rule-defeasible-unless/) and
[priority](/constructs/priority/) pages):

```ebnf
(* DECISION-0183: header parameters and body binders are mutually exclusive. *)
rule_decl               = "rule", identifier, [ rule_parameters ], rule_strength, "{",
                            { rule_item },
                          "}" ;
rule_parameters         = "(", [ rule_parameter, { ",", rule_parameter }, [ "," ] ], ")" ;
rule_parameter          = identifier, { ",", identifier }, ":", type_ref ;
rule_strength           = "strict" | "defeasible" | "defeater" ;

(* Errata E-0114: кардинальности rule_item. `when` — любое число, тело
   правила есть их конъюнкция в порядке записи (§94); `then` — любое число,
   каждая клауза даёт своё правило `<rule>/head/N` (§99); `scope`,
   `effective`, `defeat` — не более одной, повтор — LDC-E1329. *)
rule_item               = binder
                        | rule_local
                        | scope_clause
                        | effective_clause
                        | governs_clause
                        | when_clause
                        | then_clause
                        | defeat_clause
                        | unless_clause
                        | source_anchor_item
                        | "interpretation", reference_list, ";"
                        | label_item
                        | metadata_item ;

(* Errata E-0070: хвост `in expression` у биндера снят — сужение домена
   пишется конъюнктом в `when`; парсер хвост не разбирал никогда. *)
binder                  = "for", identifier, { ",", identifier },
                          ":", type_ref, ";" ;
rule_local              = "let", identifier, ":", type_ref, "=", expression, ";" ;
scope_clause            = "scope", formula, ";" ;
effective_clause        = "effective", interval_literal, ";" ;
governs_clause          = "governs", identifier, interval_literal, ";" ;
when_clause             = "when", formula, ";" ;
(* Errata E-0082: завершающая `;` у одиночного вывода необязательна —
   `us.declaration`, `eng.leviathan_1651` пишут `then duty D { … } }`, и
   `check` чист. *)
then_clause             = "then", ( conclusion, [ ";" ]
                                   | "{", { conclusion, ";" }, "}" ) ;
defeat_clause           = "defeat", proposition, ";" ;
unless_clause           = "unless", [ identifier, "when" ], formula, [ "then", proposition ], ";" ;

conclusion              = proposition
                        | norm_conclusion ;
```