Reasoning

A derive program is a set of rules (derive); its meaning is the set of tuples those rules derive. This chapter fixes that meaning: the least-fixpoint model of the positive program, the stratification that orders negation, the well-founded semantics that handles recursion through negation, and the defeasibility layer that compiles overrides onto all of it. The surface — what a derive rule looks like and what each clause is allowed to say — is in derive; this chapter is what the engine computes from it.

Least-fixpoint model

A positive derive program (no negation, no aggregation) denotes a single model: the least fixpoint of its immediate-consequence operator. Start from the ground facts, apply every rule once to derive new tuples, repeat until nothing new appears. Over a finite domain this terminates, and the result is unique — independent of the order rules fire. Multiple derive clauses with matching head name and arity union into one relation node, so a seed tuple and a recursive clause over the same head share a fixpoint (seeds ∪ derived-closure).

Aggregation extends the operator without breaking uniqueness, provided each aggregate reads a strictly lower stratum than its head writes (the stratification below). The aggregate fold then sees a converged input relation before it runs, so the fixpoint over the layered program is still unique.

Stratified negation

Negation breaks the monotonicity the least fixpoint relies on: a tuple that adds to a positive relation can remove a tuple that a not atom guarded. Stratification restores order. The rules are partitioned along their axis dependency graph — which axes a rule’s body reads against which axis its head writes — and each layer is evaluated to fixpoint before the layer above it reads its negation. A rule’s body negation must read a relation already converged in a lower stratum.

The graph must be acyclic for this layering to exist. The Lean substrate proves (Theorem 2) that a cycle in the axis dependency graph admits a Cat1/Cat2 rule pair whose stratified fixpoint is order-dependent — there is no canonical layer assignment, so the program has no single stratified model. Cross-stratum, acyclic negation is ordinary stratified negation and is evaluated by this layering.

A negation cycle that no stratification can layer — p :- not q, q :- not p — is not rejected. It is dispatched to the well-founded semantics below. (The diagnostic that once rejected such a cycle, OE1309, no longer fires from stratification; it survives only as the dispatch seam.)

Well-founded semantics

Negation reads against the well-founded model, computed by the Van Gelder–Ross–Schlipf 1991 alternating fixpoint. WFS is the default because the well-founded model always exists and is unique — every program has exactly one, with no choice for the engine to make. The headline consequence: recursion through negation is accepted. A negation cycle that strict stratification cannot layer is evaluated by the alternating fixpoint rather than refused.

The alternating fixpoint is three-valued: every atom is true, false, or undefined. The query surface is two-valued. The engine materializes only the definitely-true extent — a paradoxical atom (one the alternating fixpoint cannot pin to true or false) resolves to undefined and simply does not fire. For conditional obligations this is the sound projection: an obligation whose trigger is genuinely undecided neither fires nor is denied; it is omitted.

#[brave] / stable-model semantics — multiple two-valued models, with credulous and skeptical readings — is out of scope (Out of scope). WFS is the single evaluation discipline.

Defeasible reasoning

Real ontologies have exceptions and overrides; classical Datalog does not. Argon’s defeasibility (RFD 0028) makes them first-class without letting any rule lie about what it derives. The design has three commitments:

1. Honest heads. A rule derives exactly what its head says. An unmarked derive rule is strict — classical Datalog, exactly as derive; its conclusions cannot be overridden.
2. The attack is a directive, not grammar. Whether one rule displaces another is a statement about rules, carried in the directive plane above the rule, never a clause inside its body.
3. Strategy is a compilation scheme. The meaning of a defeasible program is the meaning of its compilation onto the core stratified/WFS semantics. No separate reasoner runs; the engine stays strategy-blind.

The directive vocabulary

The canonical example — adults can vote by default, felons are disenfranchised, special-class members vote regardless — reads true at every line:

// strict = unmarked: special-class members vote, period (unattackable)
pub derive can_vote(p) :- SpecialClass(p);

// the overridable default
#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

// the exception: an honest head, and the attack as a directive
#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

No rule spells the head it denies. The exception lives under its own name (disenfranchised); the attack rides the directive plane. The pure “block without asserting” defeater (Governatori’s ⇝) is the degenerate case — a #[defeats(…)] rule whose head no one reads.

Targeting

A #[defeats] target is resolution-checked at elaboration (goto-def-able); an unresolvable target refuses loudly. Three targeting forms ship:

• Head-level — #[defeats(can_vote(p))]: attacks every #[default] clause of that head.
• Clause-level — #[defeats(can_vote.adult(p))]: attacks exactly the clause labeled adult. This is lex specialis — the specific rule defeating the general clause’s label, an explicit cross-package-stable edge rather than a pair of magic priority integers.
• Trait-qualified — #[defeats(Vote::can_vote(p) @ A)]: attacks a trait member’s clause at a given impl target, using the qualified catalog naming (Rule-atom grammar). Exceptions compose across modules: a regulation package can defeat a clause it does not own.

Arguments resolve against the decorated rule’s variables. #[defeats(can_vote(p))] on disenfranchised(p) blocks can_vote exactly for the p the attacker derives — per-tuple blocking, not head-wide suppression. A #[defeats] argument that binds in neither the head nor the body of the rule is a loud error (OE0721), never a fresh variable.

Discipline

• Strict conclusions are unattackable (OE0717). A #[defeats] target resolving to a head or clause not marked #[default] refuses: adding rules to a classical program can only add conclusions.
• Defeat-graph cycles are refused (OE0718). The graph over resolved rule identities is acyclic by build-time check; cyclic attack structures are where the well-behaved compilation stories diverge, and Argon refuses rather than picking one silently.
• Defeated defeaters are legal — a #[defeats] rule may itself be #[default] and be attacked in turn (the exception to the exception), as long as the chain bottoms out.
• Team defeat, ambiguity blocking. A tuple is in the head’s extent iff some clause not attacked on that tuple derives it — an unbeaten teammate keeps the conclusion. A blocked tuple is simply absent from the extent; it does not propagate a third truth value downstream.
• Duplicate labels per head refuse (OE0719); labels are per-head identities.

Strategy #1: Governatori with explicit superiority

The strategy is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, specified as its Maher-2021 three-stratum compilation onto the core stratified/WFS semantics:

1. Support — run every clause (strict + default, plus the attacker rules’ own honest heads) to fixpoint over the materialized base, and attribute each clause’s contribution over that converged catalog — a recursive clause sees its own prior tuples, so transitive closure does not under-derive.
2. Blocking, from surviving attackers — project each attacker’s surviving extent (resolved in defeat-graph topological order, which exists because the graph is acyclic) through its edge argument binding to the blocked target tuples (per-tuple). A defeated defeater contributes nothing — it no longer blocks on the tuples where it was itself defeated.
3. Team-defeat fold — strict clauses contribute unconditionally; a default clause contributes the tuples no surviving edge blocks.

The strategy id is recorded in the .oxbin so an artifact is honest about which compilation gave it its meaning. Future strategies (default logic, courteous LP, argumentation, ASP preferences) arrive as use-imported macro-vocabulary packages selected per module; the engine never changes.

Proof tags

Every derived fact carries one of four tags (Rule-atom grammar), surfaced through the provenance channel (ox derive --explain):

• +Δ definitely provable — supported by a strict (unattackable) clause.
• −Δ definitely refuted.
• +∂ defeasibly provable — a surviving #[default] clause supports it after defeat resolution.
• −∂ defeasibly refuted — every supporting clause was attacked.

$ ox derive examples/legal_norms_can_vote can_vote --explain
  +Δ (dave)     // strict special-class clause
  +∂ (alice)    // surviving adult default

The Lean substrate proves the defeat algebra over each clause’s converged contribution: the team-defeat fold realizes the declarative per-tuple warranted set (Argon.Reasoning.Defeasibility.Transform.compiled_extent_eq_warranted), strict conclusions are unattackable (strict_clause_unattackable), ambiguity blocking holds (all_supporting_clauses_attacked_absent), and — modelling the blocking sets as derived from the attackers’ surviving extents rather than as opaque inputs — a defeated defeater no longer blocks (defeated_defeater_does_not_block, block_mono_in_survivors, pardoned_target_survives). The safe interaction with occurrence typing carries over — only narrowings established by strict (non-#[default]) rules are preserved under defeasible attack (Argon.TypeSystem.Soundness.Defeasibility).

Migration from the strength triple

The pre-RFD-0028 surface — #[strict] / #[defeasible] / #[defeater], #[priority(N)], and pub priority blocks — is removed, and refuses loudly (OE0722) with no silent aliasing. The map:

• #[defeasible] → #[default].
• #[defeater] (which spelled the head it denied) → an ordinary rule under its own honest head carrying #[defeats(target(args))]; the targeted clause must be #[default].
• #[strict] → delete it; unmarked rules are already strict.
• #[priority(N)] / pub priority → an explicit #[defeats] edge. Lex specialis is the specific rule defeating the general clause’s #[label]. Derived superiority (lex posterior over enactment dates) belongs to a future strategy vocabulary that derives edges.