LDC-E1302 — Contrary unless-then under a norm head

For LLMs5 sections

What it means

A rule that concludes a duty or other position cannot carry a contrary exception: unless C then not P would oppose a position that has no complement. Only the bare proviso unless C is defined under a norm head — it suspends the rule without deriving the opposite. The contrary shape stops the compiler at the exception line.

The repair is to keep the bare proviso, or to move the contrary conclusion into its own rule that derives the negated atom directly. Opposition between positions travels through dedicated patterns, never through an exception conclusion.

Example

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

entity Tenant;
relation trig(t: Tenant) kind empirical;
relation done(t: Tenant) kind institutional;
relation harm(t: Tenant) kind institutional;
rule R defeasible {
    for t: Tenant;
    when trig(t);
    then duty D {
        bearer t;
        beneficiary t;
        achieve done(t) during [@2026-01-01, infinity);
    };
    unless harm(t) then not done(t);
}

Fix

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

entity Tenant;
relation trig(t: Tenant) kind empirical;
relation done(t: Tenant) kind institutional;
relation harm(t: Tenant) kind institutional;
rule R defeasible {
    for t: Tenant;
    when trig(t);
    then duty D {
        bearer t;
        beneficiary t;
        achieve done(t) during [@2026-01-01, infinity);
    };
    unless harm(t);
}
rule Pay defeasible {
    for t: Tenant;
    when harm(t);
    then done(t);
}

Engine message

The engine reports this in its own wording:

example.law:17:5: error LDC-E1302: rule "R": the contrary `unless … then …` form under a norm head is undefined (§107.1): a position has no complement — position opposition goes via §105.1 patterns. Keep the bare `unless C` proviso or move the contrary conclusion to a separate rule

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.