When Support Is Set Aside

We have already seen how a change of information changes the answer. If a rule lacks a premise, that rule cannot derive its conclusion. If the information is declared complete, the absence of a record can become a ground for denial. Now consider one more case: the rule’s premises are established and the rule applies, but an exception sets aside its support for the conclusion.

Until now we have used strict rules, strict. Their support cannot be set aside by a defeasible rule or a defeater. That does not mean the answer stays the same under any change of data: a strict rule’s conditions must still hold. This chapter introduces rules whose support can be set aside by a separate ground even when their conditions are met.

The starting presumption

The first example comes from a study package built around a mushroom field guide. Its source is an author’s exposition with a limited list of species and identifying features[^chapter-8-source]. We study the conditions of that formalization; the study scenario’s result does not establish the edibility of a mushroom found in nature.

The object type here is called Specimen. The relation specimen(s) reports that the specimen is named in the case. The relation food_barred(s) means that eating the specimen is barred under the presumption adopted in this model. By presumption we mean the starting assumption that applies until a specified ground defeats it.

In the package that assumption is recorded by a short rule:

@source(MYCO_ART4, MYCO_ART9)
rule PresumeInedible defeasible { for s: Specimen; when specimen(s); then food_barred(s); }

The condition is familiar: the specimen is named. The conclusion is food_barred(s). The new word defeasible stands where strict stood. It means that the rule can apply while its support is later set aside. The word itself does not specify when this happens. We will see two ways to state it: a defeater that blocks support, and a priority that resolves a conflict between rules.

Start with a scenario containing a single input assertion:

test "urn:query:myco-t02-book-presumption-stands" {
    given {
        context { decision_time @2026-08-31T12:00:00Z; knowledge_time @2026-08-31T12:00:00Z; legal_time @2026-08-31; timezone "Europe/Moscow"; }
        assert specimen(entity_ref("urn:case:myco:t02")) { id "myco-t02-1"; origin case_input; }
    }
    evaluate truth(food_barred(entity_ref("urn:case:myco:t02")));
    expect result_kind == PROPOSITION;
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
    expect applied(PresumeInedible);
}

The rule applies, and there is no ground to lift its support. So food_barred receives TRUE_ONLY, and the expectation applied(PresumeInedible) checks that the named rule was applied in the justification graph.

Run the check from the reader companion directory:

law engine test \
  corpus/laws/doctrine/myco/opredelitel/tests/02-book-presumption-stands.lawtest \
  --program corpus/clir/myco-opredelitel.lawir.json --imports \
  contexts/myco-opredelitel.json

All expectations pass. A defeasible rule can yield an ordinary positive answer; its difference will show when a ground for an exception appears.

What sets support aside

The second rule links the lifting of the presumption to another established property, edible_verdict(s):

@source(MYCO_ART9)
rule FullIdentificationDefeatsBar defeater { for s: Specimen; when edible_verdict(s); defeat food_barred(s); }

The word defeater denotes a rule that blocks a defeasible conclusion. Instead of then it carries defeat, followed by the conclusion it acts upon. In our example, once edible_verdict is established, it lifts the support of food_barred that came from the presumption.

defeat food_barred(s) by itself neither concludes not food_barred(s) nor creates a permission. That is a different step: what is set aside is a particular ground of the positive conclusion[^chapter-8-defeat]. If the assertion has other surviving grounds, they too must be taken into account in reaching the answer.

Where does edible_verdict come from? In this package, strict rules first establish the species from the full set of identifying features. The rule EdibleOnlyAfterIdentification requires an established species, its assignment to the class Edible, and the negation of deadly_listed for that species. The last condition rests on declaring the list complete, using the closure introduced in the last chapter. The mere absence of the species from the list, without the remaining conditions, is not enough for the verdict.

The species’ class is stated by the package’s own information. Such entries take part in the calculation alongside the entries of a single case. So the verdict’s explanation must be traced back to the recorded features and the model’s adopted information about the species.

Support is removed, but the question remains

The supplied scenario 03 contains the full set of features specified by one entry in the identification key used in this example. Its values, such as Present or DarkBrown, are named values from the vocabulary. All starting entries live in the scenario file; below are only the two questions and their expectations:

evaluate truth(edible_verdict(entity_ref("urn:case:myco:t03")));
expect truth_status == TRUE_ONLY;
expect applied(EdibleOnlyAfterIdentification);
evaluate truth(food_barred(entity_ref("urn:case:myco:t03")));
expect truth_status == NEITHER;
expect evaluation_status == COMPUTED;

The first answer is TRUE_ONLY: the verdict rule’s conditions hold. The second is NEITHER: the presumption’s support is lifted, and there is no ground here for an explicit denial of food_barred. Compare with the third chapter: NEITHER and FALSE_ONLY mean different states.

Let us check both questions:

law engine test \
  corpus/laws/doctrine/myco/opredelitel/tests/03-book-verdict-lifts-bar.lawtest \
  --program corpus/clir/myco-opredelitel.lawir.json --imports \
  contexts/myco-opredelitel.json

Now examine the reason for the second answer. Copy the scenario 03 file used in the command above to the reader companion directory under the name bar.lawtest. Keep the header and the whole given block. Delete the first evaluate, the one about edible_verdict, and the two expect lines after it. One question about food_barred will remain, which can be handed to the explanation command:

chapter8_why_not=$(mktemp -d)
python3 reader_tools/prepare_question.py bar.lawtest \
  --program corpus/clir/myco-opredelitel.lawir.json --imports \
  contexts/myco-opredelitel.json --out "$chapter8_why_not"
law engine why-not "$chapter8_why_not"

Below is the result with the rule-application identifier shortened; the closing section on kinds of diagnostics is omitted:

статус результата: NEITHER

блокираторы (1):
  [defeated rule] urn:proof:apply:PresumeInedible:58c20198…
    побеждено по причине defeater; заключение употребление экземпляра запрещено презумпцией несъедобности(t03)

Author’s paraphrase of the engine output above (the engine’s text is in Russian and is quoted verbatim; what follows is the author’s English retelling): the result status is NEITHER, with one blocker — the application of PresumeInedible stands defeated by defeater: the presumption-based bar on eating the specimen (t03) contributes no support to the final answer.

The line defeated rule points at the set-aside application of PresumeInedible, and the reason defeater explains why its support takes no part in the final answer. The premise specimen(s) is still there. The rule applies, but a specified exception defeats its support for the conclusion.

The question about food_barred remains well-defined: we asked it and received NEITHER. That answer does not mean the absence of the bar is established. It reports that, once the exception is taken into account, there is no surviving ground either for or against the assertion.

When there is a ground for denial

Consider a second example: one rule supplies negative support, and a priority sets aside the opposing positive support. In the package on the Scrum Guide there is a type Team and three one-argument relations: scrum_team — the team is declared a Scrum team, work_visible — the work is visible to those performing and receiving it, work_hidden — the work is hidden from them.

Here it matters most to separate the text from the formalization. The Guide requires the work to be visible. That requirement by itself does not prove the work is actually visible. The presumption of visibility and the way it meets concealment are recorded in the model as further assumptions. We will examine how these assumptions work. Whether they are well-grounded calls for a separate comparison against the source.

The first rule gives the starting support for visibility:

@source(SG_S3_1)
rule WorkPresumedVisible defeasible {
    label en official "Transparency: the work of a Scrum Team is presumed visible until the contrary is established";
    for t: Team;
    when scrum_team(t);
    then work_visible(t);
}

The second yields the opposite conclusion once concealment is established:

@source(SG_S3_1)
rule HiddenWorkBreaksTransparency defeasible {
    label en official "Transparency: work hidden from those performing or receiving it is not visible";
    for t: Team;
    when scrum_team(t) and work_hidden(t);
    then not work_visible(t);
}

Both rules are defeasible. The second carries then not, not defeat: it creates support for the denial of work_visible. If a case establishes both scrum_team and work_hidden, both rules’ conditions hold. It remains to determine how to resolve their conclusions.

A priority between rules

For this pair the package holds a separate declaration:

@source(SG_S3_1)
priority HiddenWorkBeatsPresumptionOfVisibility {
    label en official "an established concealment prevails over the presumption of visibility";
    prefer HiddenWorkBreaksTransparency over WorkPresumedVisible;
    reason explicit_exception;
}

The word priority introduces a named declaration for resolving a conflict between rules. The line prefer … over … gives the concealment rule precedence over the presumption of visibility. reason explicit_exception names the reason stated in the model: an explicit exception. That is a justification mark, not an automatic proof that the source states exactly this priority[^chapter-8-priority].

In scenario 07 the team is named, and nothing is reported about concealment. The presumption yields TRUE_ONLY. In scenario 08 work_hidden is added, and the visibility question receives FALSE_ONLY. The presumption’s positive support is set aside by priority, while the second rule’s negative support survives.

The second case can be checked with this command:

law engine test \
  corpus/laws/org/scrum/guide/tests/08-book-hidden-work-prevails-by-priority.lawtest \
  --program corpus/clir/scrum-guide.lawir.json --imports contexts/scrum-guide.json

The reason the presumption was set aside will be shown by:

chapter8_why_not=$(mktemp -d)
python3 reader_tools/prepare_question.py corpus/laws/org/scrum/guide/tests/08-book-hidden-work-prevails-by-priority.lawtest \
  --program corpus/clir/scrum-guide.lawir.json --imports contexts/scrum-guide.json \
  --out "$chapter8_why_not"
law engine why-not "$chapter8_why_not"

Unlike the field guide, the final status here is FALSE_ONLY, and the set-aside rule’s line carries the reason priority. These are two differences to be read together: what remains in the answer, and why the other ground was set aside.

What happens without the priority

Let us check the third declaration’s role with a separate trial. As in the sixth chapter, make a copy of the package. The commands run from the reader companion directory in one terminal window:

chapter8_work=$(mktemp -d)
cp -R corpus/laws/org/scrum/guide "$chapter8_work/guide"

In the file 02-theory.law inside the copy, delete only the declaration HiddenWorkBeatsPresumptionOfVisibility together with its @source(SG_S3_1) line. Keep both rules. Then prepare the changed model and repeat the starting scenario 08:

law engine lower "$chapter8_work/guide" > "$chapter8_work/without-priority.lawir.json"
law engine test \
  corpus/laws/org/scrum/guide/tests/08-book-hidden-work-prevails-by-priority.lawtest \
  --program "$chapter8_work/without-priority.lawir.json" --imports \
  contexts/scrum-guide.json

The FALSE_ONLY expectation will fail: the result is BOTH. In this trial both opposing supports survive, since the preference between them is removed. The order of the rules in the file does not replace a priority.

If you copy the scenario and change the expected status to BOTH, the check will pass. It will confirm the changed model’s behaviour, not establish that the model faithfully reads the Guide. Restoring the priority and running lower again returns the starting scenario’s result.

Compare the cases considered:

These are the results of particular sets of rules and information. The mere presence of a defeater never promises NEITHER, nor does a priority always promise FALSE_ONLY: the outcome depends on all surviving grounds for the stated assertion.

Try it yourself

1. In a copy of the field guide’s scenario 03, delete only the myco-t03-6 entry about the spore print. Predict both answers, then run the check with the old expectations. After accounting for the mismatches, correct the expectations. To examine the answer about food_barred, keep only the second question in a separate copy, as done above.
2. In a copy of the Scrum scenario 08, delete only the sg-t8-b entry about the work’s concealment. Predict the state of work_visible and the applied rule. First check the old expectations, then change them for the revised case.
3. After the trial without priority, restore the deleted declaration in the package copy, run lower again, and start the untouched scenario 08. Explain which support is now set aside and which survives.

Check your predictions

In the first exercise the full set of identifying features is no longer established, so the species is not identified. edible_verdict will receive NEITHER, and the expectation of applying EdibleOnlyAfterIdentification must go. food_barred will be TRUE_ONLY: the defeater’s condition fails, and the presumption’s support survives.

In the second exercise visibility will receive TRUE_ONLY; replace the expectation of applying the concealment rule with applied(WorkPresumedVisible). In the third, the restored priority leaves the negative support standing again, and the starting check with FALSE_ONLY passes.

We have learned to distinguish a rule that did not apply, a support that was set aside, and support for a denial. In all three cases the explanation leads to different grounds, even when the answer states sometimes coincide. The next chapter adds one more source of differences: a decision that must come not from the model but from a person named in it.

The English wording of the Scrum rules and priorities in this chapter is quoted verbatim from the package, which follows the English original of the Guide; the surrounding prose retelling is the translator’s own.

[^chapter-8-source]: The author’s exposition and its articles; the verdict, presumption, and defeater rules. Scenarios 02 and 03 check the presumption’s two sides. [^chapter-8-defeat]: The Arxo specification, §§104, 107–108: applicability, defeat, and surviving support. A defeater attacks defeasible support; strict support cannot be lifted that way. [^chapter-8-priority]: Fragment SG_S3_1 records the visibility requirement; 02-theory.law states the formal rules and the priority. Their action is checked by scenarios 07 and 08.