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.

OverviewBoundariesCorpus formsPitfalls

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)

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).

Arxo 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:

Output

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:

Arxo 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, 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 (defeasible rules, unless, defeater), negation (negation), 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

Show syntax reference

Productions of the rule_decl family (strict strength is one alternative of rule_strength; defeat and priority live on the defeasible rules and priority pages):

Grammar

(* 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 ;