Why this answer was obtained

A “not established” answer is formalised law’s most frequent answer and its most dangerous: three different things stand behind it. The norm is absent from the model; the norm exists but did not fire for lack of a premise; the premise exists but the case fact did not match it. These are different answers, and none may be passed off as another. This page is about how the core tells them apart: the proof graph, the refusal explanation, the query modes, and the tools above them.

Arxo Law

language "law.core" version "0.2";
package tutorial.archive version "0.15.0";
namespace "urn:law:tutorial:archive";

import tutorial.city version "0.1.0";

entity Person;
entity CopyOrder;

relation billing_year(p: Person, year: Integer) kind empirical { key(p); }
relation copy_order(o: CopyOrder, p: Person, pages: Integer) kind empirical { key(o); }
relation copy_fee(o: CopyOrder, amount: Money) kind institutional { key(o); }
relation copy_fee_computable(o: CopyOrder) kind institutional;

rule CopyFeeComputable strict {
    label ru-KZ unofficial "Плата за копирование вычислима: есть заказ, год счёта и ставка города на этот год";
    for o: CopyOrder;
    for p: Person;
    for n: Integer;
    for y: Integer;
    for rate: Money;
    when copy_order(o, p, n) and billing_year(p, y) and tutorial.city::base_page_rate(y, rate);
    then copy_fee_computable(o);
}

rule CopyFee strict {
    for o: CopyOrder;
    for p: Person;
    for n: Integer;
    for y: Integer;
    for rate: Money;
    when copy_order(o, p, n) and billing_year(p, y) and tutorial.city::base_page_rate(y, rate);
    then copy_fee(o, n * rate);
}

The label reads: “Copy fee is computable: there is an order, a billing year, and the city rate for that year”.

What the answer composed of

When there is an answer, it has a proof. The proof graph stores every step: a case statement, a rule application, a query. The explanation command prints the chain from the question to the leaves:

Output

$ lawc explain <каталог с ir.json, case.json, query.json>
copy_fee(order1, 1050): TRUE_ONLY
  rule_application  copy_fee(order1, 1050)
    (urn:proof:apply:CopyFee:3383fcd9…)
    assertion  copy_order(order1, ivanova, 7)
      (urn:proof:assert:urn:law:tutorial:archive#assert-order)
    assertion  billing_year(ivanova, 2026)
      (urn:proof:assert:urn:law:tutorial:archive#assert-year)
    assertion  базовая ставка платы за страницу копии, установленная городским советом на год(2026, 150)
      (urn:proof:assert:urn:law:tutorial:city#city-page-rate-2026)

The command takes “a directory with ir.json, case.json, query.json”; the last leaf reads “the base copy page rate set by the city council for the year (2026, 150)”.

Three leaves under one application, the third from a foreign package: the rate arrived as a tutorial.city fact, and the graph names it by StableId together with the label. The graph command prints the same in DOT. In the evaluation document the graph lies next to the result. The test from this page, byte for byte:

Arxo Law

test "плата вычислена — ставка совета в доказательстве" {
    given {
        context {
            decision_time @2026-04-20T09:00:00+05:00;
            knowledge_time @2026-04-20T09:00:00+05:00;
            legal_time @2026-04-20;
            timezone "Asia/Almaty";
        }
        assert billing_year(entity_ref("urn:tutorial:ivanova"), 2026) {
            id "assert-year";
            origin case_input;
        }
        assert copy_order(entity_ref("urn:tutorial:order1"), entity_ref("urn:tutorial:ivanova"), 7) {
            id "assert-order";
            origin case_input;
        }
    }
    evaluate truth(copy_fee(entity_ref("urn:tutorial:order1"), 1050 KZT));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

The test name reads: “The fee is computed — the council rate is in the proof.”

A test’s applied(Rule) observation reads the same graph: it is true when the proof nodes include an application of the named rule. Inside a page-package this observation cannot be compiled (like position and issue — a call of an undeclared function), so in the page’s test file it stands as separate scenarios:

Output

evaluate truth(copy_fee(order1, 1050 KZT));           expect applied(CopyFee);
evaluate truth(copy_fee_computable(order1));           expect not applied(CopyFeeComputable);   // счёт за 2025

The comment reads “billed for 2025”.

Why there is no answer

Billed for 2025, for which the council set no rate. The answer is NEITHER — and the question is “why”. The refusal explanation is built by the why-not command: for each rule with the needed head it names whether the rule applies and what holds of each premise.

Output

$ lawc why-not <каталог>        # вопрос copy_fee_computable(order1)
статус результата: NEITHER

блокираторов, подтверждённых документом, нет

не определено (1) — условие НЕ опровергнуто, вывода просто нет:
  urn:law:tutorial:archive#CopyFeeComputable
    правило … не сработало, но условие НЕ опровергнуто:
    базовая ставка платы за страницу копии, установленная городским советом
    на год(?v3, ?v4) — переменные не связаны целью: v3, v4;
    copy_order(?v0, ?v1, ?v2) — переменные не связаны целью: v1, v2;
    billing_year(?v1, ?v3) — переменные не связаны целью: v1, v3

The report reads: the question is copy_fee_computable(order1); “result status: NEITHER”; “no document-confirmed blockers”; “undetermined (1) — the condition is NOT refuted, there is simply no derivation”; “rule … did not fire, but the condition is NOT refuted”; then the premises with “variables unbound by the goal”.

Three kinds of refusal differ in words. A blocker is a premise refuted by the document: a case fact or a norm established FALSE_ONLY. Undetermined means a premise is neither refuted nor established: the rule stays silent, and the silence is named. And the third, absent here, is that no rule with this head exists at all: then the report says “no program rule holds this predicate in its head; the value can only arrive as a case fact”. The first is “law refused”, the second “law stays silent”, the third “the norm is not in the model”. Three different answers to a lawyer.

Billing year	copy_fee_computable(order1)	applied(CopyFeeComputable)
2026	TRUE_ONLY	yes
2025	NEITHER	no

A simple head for investigation

Note the question targets copy_fee_computable, not copy_fee. That is no accident. Ask why-not about copy_fee(order1, 1050 KZT) and the report is empty: neither blockers nor “undetermined”. The copy_fee head is computed, n * rate, and the refusal analysis requires the argument value to match before reaching the premises: “1,050 not derived” is indistinguishable to it from “no rule”. Hence corpus calculation packages guard input completeness with a separate simple-headed predicate, while computed rules read it as a premise. Ask “is it computable”, and the report names the missing premise by name.

Five query modes

Until now the pages asked truth. There are five query modes, each with an answer of its own form:

Mode	Question	Answer
truth	is the literal established	four states, proof, whyNot
collect	which substitutions satisfy the formula	a value collection; completeness depends on producer completion
deadline	when the term expires	a date by the counting policy and the calendar
calc	what the term equals	a value and kind (DATA); in a test — expect value
positions	which positions the case holds	duty, ban, and power statuses

In scenario tests they are written evaluate truth(…), evaluate collect …, evaluate deadline(…), evaluate <term>, evaluate positions(); in tools as a mode parameter. A mode does not change law: one case and one program give consistent answers in all five.

Tools above the answer

Everything the explanation and why-not commands print is in the evaluation document itself: proof, whyNot, issues, a manifest with the program and case hashes. The tools only read it:

• law_ask answers by case and, when “not established”, carries whyNot with each premise’s status; the answer’s legal order is named by the acts that fired, not by the import closure;
• law_explain prints the derivation chain; law_argue the conclusion’s strength: what defeats it, which priorities hold;
• law_sources — where the norm is from and what pins its text.

None of them computes law itself (invariant 5): the answer arrives from the CLIR implementation; the tool shows it. Byte pinning, hashes, and compilability guard the answer’s technical properties; interpretation correctness is established by scenarios — tests with expectations someone read with eyes.

Next

The answer is explained; what remains is making the package a corpus package — with a manifest, declared scenarios, provenance, and registration in checks: the track’s last page.