General rule with an exception

Intention

I want to lift a general rule by carrying the bound person into the exception itself.

A person bound only in the general rule body is not automatically bound in the exception.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

Incorrect form

unless lost(item);

The general-rule body is not carried into the exception: p remains an unbound variable of the generated defeater.

Correct form

Arxo Law

language "law.core" version "0.2";
package recipes.b.r01 version "0.1.0";
namespace "urn:recipe:b-rules:01";

entity Person;
entity Item;
relation owns(p: Person, item: Item);
relation lost(item: Item);
relation allowed(p: Person, item: Item);
rule General defeasible {
    for p: Person; for item: Item;
    when owns(p, item);
    then allowed(p, item);
    unless owns(p, item) and lost(item);
}

Frozen execution scene

Facts and choice	Question	Answer
item with the owner	truth(allowed(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")))	TRUE_ONLY / COMPUTED
item lost	truth(allowed(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")))	NEITHER / COMPUTED
proviso removed	truth(allowed(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")))	TRUE_ONLY / COMPUTED

item with owner

Arxo Law

test "item with owner" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert owns(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a"));
    }
    evaluate truth(allowed(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

item lost

Arxo Law

test "item lost" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert owns(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")); assert lost(entity_ref("urn:recipe:b-rules:01:a"));
    }
    evaluate truth(allowed(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
}

exception removed

Arxo Law

test "exception removed" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert owns(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")); assert lost(entity_ref("urn:recipe:b-rules:01:a"));
    }
    evaluate truth(allowed(entity_ref("urn:recipe:b-rules:01:p"), entity_ref("urn:recipe:b-rules:01:a")));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

Counterfactual

Mutation: unless owns(p, item) and lost(item); → unless lost(item);; rejection LDC-E4101. Scenes that delete a fragment are marked explicitly in the table.

Boundary

A bare unless blocks the conclusion rather than establishing its negation. The contrary form is An exception establishes negation.

Pitfall

Bind the same person in the exception: a variable bound only in the general rule body stays unbound in the generated defeater.