Constraints

In one sentence: constraint expresses a mandatory relation between the already established (facts, positions) but infers nothing: the when antecedent true and the require requirement false is a violated/conflicted/undetermined finding in the results, not a new fact and not a sanction. The author takes it when a case’s coherence must be checked without making the checked inferable.

The language specification treats a constraint as a check, not an inference: when the antecedent holds and the requirement fails, the engine writes a finding, adds no support, and imposes no sanction. Prohibitions — norms with a holder, a window, and a lifecycle — live on the prohibitions page.

OverviewBoundariesCorpus formsPitfalls

1. When to use and when not to

Instead	Selection rule
constraint vs rule strict	A rule infers the consequent as a new fact with support; a constraint adds no logical support. If Y must follow from X, write a rule; if a case with X but without Y is incoherent, a constraint. X only_if Y desugars exactly into a constraint, not into a rule
constraint vs prohibition	A prohibition is a norm with a holder, a window, and a lifecycle; a constraint is a validation finding without holder or window, computed on every evaluation. A prohibition’s violation is a position violation; a constraint’s failure is a finding without sanction: a sanction is encoded by a separate rule on established facts
constraint vs definition … necessary	A definition’s necessary half is also a constraint (“concept requires condition”) but with the was_derived_from provenance edge and a place in the theory. A one-off coherence condition is a bare constraint; a condition entering a concept is a definition
require vs a power’s valid_when	valid_when is an exercise-validity condition: without it the effect does not materialize. require is a coherence check without effect: without it nothing is extinguished, only a finding is written

2. Minimal example

Package research.constraint.enrolled_needs_consent: a child’s enrolment requires a guardian’s consent. Consent is inferred by a rule from a fact; the constraint only checks coherence.

Arxo Law

rule ConsentFromGuardian strict {
    for c: Child;
    for g: Guardian;
    when consent(g, c);
    then has_consent(c);
}

constraint EnrolledNeedsConsent(c: Child) {
    when enrolled(c);
    require has_consent(c);
    severity error;
    message "зачисление требует согласия законного представителя";
}

Case 01 facts: enrolled(ann) + consent(maria, ann). Query: evaluate truth(has_consent(ann)).

Actual engine answer:

Output

law test research.constraint.enrolled_needs_consent: мир research.constraint.enrolled_needs_consent
  ok   [research.constraint.enrolled_needs_consent#authored] tests/01-consent-present.lawtest / urn:query:research-constraint-01
  ok   [research.constraint.enrolled_needs_consent#authored] tests/02-consent-missing.lawtest / urn:query:research-constraint-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0

law engine check — check OK, no warnings.

Sensitivity is double. First, removing the consent fact changes the answer to the same query from Established to Not established, not refuted (the consent-missing test): the constraint did not infer has_consent from enrolled — the key property (“adds no logical support”) visible right in the run. Second, the constraint’s own verdict follows the verdict table: antecedent Established + requirement Established → satisfied (case 01, no issue), antecedent Established + requirement Not established, not refuted → undetermined with missing_inputs (case 02). The law test output shows only query statuses — findings live in the results with a constraint result kind, which was not printed separately in these runs.

Second package research.constraint.certified_needs_test — the same device in the standards domain with severity warning: certified equipment must hold a passed test record. Case 02 (record present, certificate absent) answers Established on the record query: the constraint is untriggered without the antecedent and stays silent — no finding. Runs — 2/2, check OK.

3. Example by domain

• Religion (inheritance fiqh): package faraid.shares (Faraid inheritance shares, Islamic law) — constraint SonImpliesMaleDescendant (see the corpus forms): a declared son means an inheriting male-line descendant; inference by rule is deliberately forbidden, otherwise negation on has_male_descendant would stop working. Exemplary “check, don’t infer”.
• Standard (IFRS): package eu.ias.provisions (IAS 37, provisions) — constraint Para14RequiresPresentObligation: a recognised provision requires a present obligation; severity error with an expanded message from the paragraph 14 text.
• Custom: package custom.warlpiri.kinship (Warlpiri kinship, Australian customary law) — constraint WrongSkinMarriageConstraint: Warlpiri marriage classes as case incoherence, not as a holder-bearing prohibition.
• Teaching cases: package research.constraint.enrolled_needs_consent (guardianship, severity error), package research.constraint.certified_needs_test (standard, severity warning).

4. How the engine answers

Table — actual runs of this section’s teaching packages (query statuses):

Facts	Question	Answer	Why
enrolled, consent	has_consent	Established	rule inferred; constraint satisfied, no issue
enrolled	has_consent	Not established, not refuted	constraint infers nothing; its verdict is undetermined
certified, lab_passed	test_passed	Established	rule inferred; constraint satisfied
lab_passed	test_passed	Established	rule fires without certificate; constraint untriggered and silent

The full verdict table (antecedent Established × requirement Established/Refuted/Contradiction/Not established, not refuted → satisfied/ violated/conflicted/undetermined; a conflicted antecedent → conflicted). In 0.2 a constraint evaluates on every evaluation — after all strata and the norm runtime, before the answer. The result is a results element with a constraint result kind, applicable status, and a stable runtime id; the constraint_check proof node is a graph root. A violated verdict gives issue CONSTRAINT_VIOLATED, conflicted gives CONSTRAINT_CONFLICTED; satisfied and undetermined produce no issue. severity critical is written as error with details.severity = "critical". These details were not printed separately in the section’s runs and are stated from the language description.

Grounding: which substitutions are checked

Substitutions are enumerated over the positive binding literals of the scope-and-when conjunction. Enumeration includes atoms with Contradiction status: a contradictory antecedent is a finding (conflicted), not a reason to hide it. A substitution whose antecedent support pair is negative-only is untriggered — it has no result. For an undetermined verdict, the missing_inputs field names the requirement literals with Not established, not refuted status. The implicit-established wrapper (require age(p) lowers to established(age(p)), like a body literal) reads four-valued — otherwise Contradiction/Not established, not refuted outcomes would not exist; other status tests (not_known, supported, refuted, unknown) stay boolean.

A judge in requirement: the requirement can carry the judgment channel. On an undetermined verdict with an open judge, the result carries an evaluation status of REQUIRES_JUDGMENT and judgment_requests with constraint addresses; the verdict and missing_inputs are unchanged.

5. Common mistakes

1. Expecting inference from a constraint: require Y does not establish Y — Not established, not refuted where the author expected Established (pitfalls, item 1).
2. Expecting a sanction: a constraint’s failure is a finding, a violation is inferred from a position instance by a separate rule (pitfalls, item 2).
3. A constraint as a producer: the “constraint reads what it infers” cycle — a constraint cannot be a producer for its strata (pitfalls, item 3).
4. Repeated scope/effective, silently skipped body elements — LDC-E1329/LDC-E0201 (pitfalls, item 4).
5. effective outside the law date: the constraint silently does not apply (pitfalls, item 5).
6. An unexecutable body: formulas outside the executable subset — issue NON_EXECUTABLE_CONSTRAINT, the constraint is not evaluated (pitfalls, item 6).

6. References

• Neighbour pages: prohibitions, definitions, powers.
• The pitfalls page lists the diagnostics (LDC-E1329, LDC-E0201) with wrong forms and fixes.