Facts and evidence

In one sentence: assert lays support — positive or negative — on a ground atom: rules infer from supports, while provenance (origin), times (valid/observed/recorded), and documents (evidence) say where the support came from and when it holds. The author takes a fact when an inference needs a premise: without an established premise the rule stays silent, and the question answers Not established, not refuted.

The language specification treats a fact as support laid on a ground atom: rules infer from supports, while provenance, times, and documents say where the support came from and when it holds. Package facts state the act’s standing data; case facts state one computation’s input.

OverviewBoundariesCorpus formsPitfalls

1. When to use and when not to

Instead	Selection rule
assert p(x) vs assert not p(x)	An established fact is positive support; an established absence is negative support. Absence of a fact is not negation: without not the question never gives Refuted. Criterion: the organ recorded the absence — not; data simply missing — nothing
origin case_input vs origin source_asserted	A fact of the case side is case_input; an assertion of the act itself, visible in every case against the package, is source_asserted (the package-fact default). The origin list is closed: a typo is LDC-E1374, not “a new provenance kind”
A package fact vs a case fact (given)	The act’s handbook (rate, vocabulary, an organ decision with a date) is a package fact: always visible. One computation’s input is the case: the program is presented separately, the case cannot change law. Both supplies add into one support store — a case fact does not “override” a package fact but disputes it (Contradiction)
valid [a, b) vs observed/recorded	valid is when the assertion is true of the world: checked against the law date, a non-covering fact does not enter supports (ASSERTION_OUTSIDE_VALID). observed/recorded are bitemporal qualifiers: compared with nothing except order between themselves (LDC-E3101)
evidence Name; vs a document in the package	A document reference lives in the fact, the document itself is a case input. An evidence declaration in the package is warning LDC-E1314: a document is not part of the program

2. Minimal example

Package research.facts.polarity: “Acme” registration — a positive package fact, absence of liquidation — a negative one; the rule reads both premises plus a licence from the case:

Arxo Law

assert registered(entity_ref("urn:case:research:facts:acme")) {
    id "assert-acme-registered";
    origin source_asserted;
}
assert not in_liquidation(entity_ref("urn:case:research:facts:acme")) {
    id "assert-acme-not-in-liquidation";
    origin source_asserted;
}
rule MayTrade strict {
    for c: Company;
    when registered(c) and licensed(c);
    then may_trade(c);
}

Case facts: licensed(acme) with origin case_input. Query: evaluate truth(may_trade(acme)) — both premises Established (the package fact is visible in an empty case).

Actual engine answer:

Output

law test research.facts.polarity: мир research.facts.polarity
  ok   [research.facts.polarity#authored] tests/01-may-trade.lawtest / urn:query:research-facts-01
  ok   [research.facts.polarity#authored] tests/02-no-support.lawtest / urn:query:research-facts-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0

law engine check — check OK, no warnings. Sensitivity: an empty case (no licensed) gives may_trade = Not established, not refuted (the no-support test): the package fact registered gives support, but the second premise is missing — the rule stays silent.

Second package research.facts.valid_window: an audit exemption with window valid [@2027-01-01, infinity). Actual answer: law date 2027-06-01 — Established (the inside-window test); law date 2026-03-01 — Not established, not refuted (the outside-window test), law test — 2/2. Sensitivity is on the law date, not on the fact: one and the same fact enters supports or not depending on the law date. The window is half-open: the first day is included.

Nearest wrong outcome: reading off-window Not established, not refuted as “no fact”. The fact exists — it is not accepted into supports, and the engine attaches issue ASSERTION_OUTSIDE_VALID (info). A guard test must distinguish “no support” from “support not accepted”, otherwise window silence is indistinguishable from a missing fact.

3. Example by domain

• Law (health insurance): package kz.corpus.osms (Mandatory Social Health Insurance, Kazakhstan) — block assert defined_term(…) with the term’s text as label: the act’s vocabulary as facts, the term as the value, the text as the label.
• Science (grammar): package kz.grammar.lexicon (Kazakh language lexicon) — pub facts KirispeMysaldary with qualified neighbour facts: exporting a fact vocabulary across the package boundary.
• Regulator: package kz.national_bank.fx (National Bank of Kazakhstan, exchange rates) — one-line assert reference rates: a package fact as part of the program, visible in every case.
• Teaching case: package research.facts.valid_window — a valid window in miniature: the same mechanics of dated organ decisions as in acts with an effective date.

4. How the engine answers

Table — actual runs of this section’s teaching packages:

Facts	Question	Answer	Why
package fact registered, case licensed	may_trade(acme)	Established	both premises established
package fact, empty case	may_trade(acme)	Not established, not refuted	no licensed premise
valid window from 2027, law date 2027-06-01	exempt_from_audit(acme)	Established	window covers the law date
same window, law date 2026-03-01	exempt_from_audit(acme)	Not established, not refuted	fact not in supports; issue ASSERTION_OUTSIDE_VALID

Additionally, further checked behaviours of the earlier edition (not fixed by a run in these teaching packages):

Case facts	Question	Answer	Why
nothing	registered(beta)	Established	an anonymous fact is the same kind of fact
nothing	in_liquidation(acme)	Refuted	a negative package fact
nothing	licensed(acme)	Not established, not refuted	no support at all — not Refuted
not licensed	licensed(acme)	Refuted	a negative case support
licensed, not licensed	licensed(acme)	Contradiction	both polarities preserved
licensed, not licensed	may_trade(acme)	Not established, not refuted	a Contradiction premise does not activate the rule
not registered	registered(acme)	Contradiction	a case fact does not cancel a package fact — it disputes it
licensed with a case document	licensed(acme)	Established	a fact with a case document
licensed with origin assumed_for_simulation (mode not simulation)	licensed(acme)	Not established, not refuted + ASSERTION_NOT_ACCEPTED	the assumption is not accepted

• Supports add up, they are not overwritten: case not licensed plus case licensed is Contradiction, not cancellation; a case fact against a package fact is a dispute (Contradiction), not an override. On these teaching packages the addition of opposite supports is not fixed by a run — the claim is marked here as “not checked”.
• A rule body reads established: a Contradiction premise does not activate the rule — the same mechanics as on the strict-rules page.
• Provenance is modal: an assumed_for_simulation assumption outside simulation does not reach supports — Not established, not refuted with warning-issue ASSERTION_NOT_ACCEPTED. Not checked on examples: both examples are case_input/source_asserted.
• An anonymous fact in 0.2 gets its id from content: <namespace>#assert-h<sha256>; two exact anonymous duplicates are a rejection LDC-E1331.

Note on fact addressing: an explicit id is needed where the fact is referenced from outside the file — proof-graph premises address it by StableId, and a case is hashed whole, so the case hash must not change on renumbering. The short spelling is a string before the colon (assert "a": licensed(…) { origin case_input; }): the same id field as in the block — exactly how all case facts in this section’s teaching packages are written. An anonymous package fact (no id) is the same kind of fact: in 0.2 it gets a content-derived id, and rules read it equally with a named one.

5. Common mistakes

1. The fact exists but the rule stays silent: a Contradiction premise, an unaccepted fact, or a value mismatch (pitfalls, item 1).
2. Two identical anonymous facts — LDC-E1331 (pitfalls, item 2).
3. A valid window in the future with today’s law date — silent Not established, not refuted (pitfalls, item 3).
4. A typo in origin — LDC-E1374 (pitfalls, item 4).
5. A rule in given — a case carries no law (pitfalls, item 5).
6. An evidence declaration in the package — LDC-E1314 (pitfalls, item 6).
7. A computation in a fact argument — LDC-E1325/LDC-E1324 (pitfalls, item 7).

6. References

• Neighbour pages: strict rules, vocabulary, negation.
• The first-package and defeaters tutorials live in the tutorials catalogue.
• The pitfalls page lists the diagnostics (LDC-E1331, LDC-E1374, LDC-E1314, LDC-E1325/LDC-E1324, LDC-E3101) with wrong forms and fixes.

7. Grammar excerpts

Show syntax reference

An assertion and its qualifiers (the assertion_decl, assertion_item productions):

Grammar

assertion_decl          = "assert", [ string_literal, ":" ], proposition,
                          [ "{", { assertion_item }, "}" ],
                          [ ";" ] ;
assertion_item          = "valid", interval_literal, ";"
                        | "observed", temporal_literal, ";"
                        | "recorded", temporal_literal, ";"
                        | "evidence", reference_list, ";"
                        | "origin", identifier, ";"
                        | stable_id_item
                        | source_anchor_item
                        | label_item
                        | metadata_item ;

A fact group and its inclusion (the facts_decl, facts_use_decl productions; inclusion is an explicit facts package::Name; line):

Grammar

facts_decl              = "facts", identifier, "{",
                            { assertion_decl | label_item },
                          "}" ;