Missing and conflicting facts

Arxo works in an open world: a fact that nobody stated is unknown, not false. Every statement therefore has four possible answers, and a package can say explicitly when silence should count as denial. This page shows all four answers on the parking-permit rule, and the command that explains a “not established”.

Open this package in the playground → — edit the rules and the scenarios of this page and run them in your browser.

The package

language "law.core" version "0.2";
package demo.parking version "0.1.0";
namespace "urn:law:demo:parking";

entity Applicant;

relation applicant_on_file(a: Applicant) kind institutional;
relation resident(a: Applicant) kind institutional;
relation vehicle_registered(a: Applicant) kind institutional;
relation permit_eligible(a: Applicant) kind institutional;

rule PermitEligibility strict {
    for a: Applicant;
    when resident(a) and vehicle_registered(a);
    then permit_eligible(a);
}

One addition: the town keeps a complete register of residents. A closure declares that completeness for one predicate over one domain — for every applicant on file, absence of a residence record is an explicit “not a resident”. The declaration names the snapshot it relies on and the moment it was complete.

closure ResidentsRegister {
    predicate resident;
    domain applicant_on_file;
    snapshot "urn:snapshot:demo-parking-residents:2026";
    complete_as_of @2026-01-01T00:00:00Z;
    derive_explicit_negative true;
}

The four answers

Each answer is a pair: is there support for the statement, is there support against it.

Answer	Support for	Support against	Reads as
TRUE_ONLY	yes	no	established
FALSE_ONLY	no	yes	refuted
NEITHER	no	no	not established, not refuted
BOTH	yes	yes	contradictory input or unresolved conflict

Nothing is known. The case is empty; the rule does not fire, and nobody said Ann is not eligible.

test "silence: nothing is known about Ann" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:parking:ann")));
    expect truth_status == NEITHER;
    expect not applied(PermitEligibility);
}

Denial is an input. assert not … is a fact like any other: it puts support against the statement.

test "denial: Ann is stated not to be a resident" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert not resident(entity_ref("urn:demo:parking:ann")) { id "ann-not-resident"; origin case_input; }
    }
    evaluate truth(resident(entity_ref("urn:demo:parking:ann")));
    expect truth_status == FALSE_ONLY;
}

Contradiction is preserved. Two records disagree about Ann’s residence. Neither cancels the other; the answer is BOTH, and a rule that needs resident(a) established does not fire on a disputed premise.

test "contradiction: two records disagree" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert resident(entity_ref("urn:demo:parking:ann")) { id "ann-resident"; origin case_input; }
        assert not resident(entity_ref("urn:demo:parking:ann")) { id "ann-not-resident"; origin case_input; }
        assert vehicle_registered(entity_ref("urn:demo:parking:ann")) { id "ann-vehicle"; origin case_input; }
    }
    evaluate truth(resident(entity_ref("urn:demo:parking:ann")));
    expect truth_status == BOTH;
}

test "a disputed premise does not fire the rule" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert resident(entity_ref("urn:demo:parking:ann")) { id "ann-resident"; origin case_input; }
        assert not resident(entity_ref("urn:demo:parking:ann")) { id "ann-not-resident"; origin case_input; }
        assert vehicle_registered(entity_ref("urn:demo:parking:ann")) { id "ann-vehicle"; origin case_input; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:parking:ann")));
    expect truth_status == NEITHER;
    expect not applied(PermitEligibility);
}

Declared closure turns silence into denial — inside its domain. Carl is on file but has no residence record: the register is complete, so he is not a resident. Dana is not on file at all, and the closure says nothing about her.

test "closure: on file without a record means not a resident" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert applicant_on_file(entity_ref("urn:demo:parking:carl")) { id "carl-on-file"; origin case_input; }
    }
    evaluate truth(resident(entity_ref("urn:demo:parking:carl")));
    expect truth_status == FALSE_ONLY;
}

test "closure: outside the domain silence stays silence" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert applicant_on_file(entity_ref("urn:demo:parking:carl")) { id "carl-on-file"; origin case_input; }
    }
    evaluate truth(resident(entity_ref("urn:demo:parking:dana")));
    expect truth_status == NEITHER;
}

Why not?

A NEITHER has a reason, and the engine names it. Put a single scenario in its own file — tests/only-residence.lawtest, Ann is a resident and nothing else is known — and ask why the conclusion was not reached:

test "only residence is known" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert resident(entity_ref("urn:demo:parking:ann")) { id "ann-resident"; origin case_input; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:parking:ann")));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
}

law engine why-not tests/only-residence.lawtest --program parking.law --json

The answer names the rule that did not fire and the premise that stopped it (the human-readable detail strings are shortened here):

{
  "status": "NEITHER",
  "blockers": [],
  "observations": [
    {
      "kind": "не определено",
      "subject": "urn:law:demo:parking#PermitEligibility",
      "detail": "… vehicle_registered(ann) … NEITHER"
    }
  ],
  …
}

blockers is empty: nothing refuted the premise. The observation says the rule was applicable and one of its premises, vehicle_registered(ann), is NEITHER. The same explanation is available from application code as whyNot — see Coming from Catala.

Run it

law engine check parking.law
law engine test tests/four-answers.lawtest --program parking.law

check OK: parking.law

test PASS: silence: nothing is known about Ann
test PASS: denial: Ann is stated not to be a resident
test PASS: contradiction: two records disagree
test PASS: a disputed premise does not fire the rule
test PASS: closure: on file without a record means not a resident
test PASS: closure: outside the domain silence stays silence

Try one change

Change derive_explicit_negative true to false in the closure. The register is still declared, but it no longer produces denials: Carl’s answer becomes NEITHER, and the fifth scenario fails:

test FAIL: closure: on file without a record means not a resident
  truth_status == FALSE_ONLY: в документе NEITHER