Markdown for LLMs
Strict rules
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# 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 ;
```