Markdown for LLMs
Why this answer was obtained
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# 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.
```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:
```text
$ 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:
```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:
```text
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.
```text
$ 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](/tutorials/package/).