Robot plan execution: three reasoning regimes on one model

Area: Rules, aggregates & recursion Teaches: a planning/robotics domain over a self-defined upper ontology, exercising three workhorse reasoning regimes on one package — a true bounded forall, a mutually-recursive least fixpoint, and arbitration by recursion through negation under well-founded semantics. Also: an upper ontology is an ordinary module, not a language built-in. Prerequisites: first-class relations; derive rule bodies; negation-as-failure. Run: ox build examples/robot_plan_execution && ox query examples/robot_plan_execution

A mobile robot executes a plan: charge, navigate, scan, pick up. Two modules split the model deliberately — upper is a minimal upper ontology defined in this package (Object, Event, Capability, a derived involves), and robot specializes it (Agent <: Object, Action <: Event, Skill <: Capability) and builds the planner. Argon is ontology-neutral: a published foundational ontology could be imported in upper’s place without touching the domain.

What to read in robot.ar

A true universal — the bounded forall. An action is ready-at-start when every one of its preconditions holds initially. This lowers to a count-equality, not the existential “some precondition holds” (an action with no preconditions is vacuously ready):

pub derive readyAtStart(a: Action) :-
    Action(a),
    forall f: Fluent where pre(a, f), holds(f);

A mutually-recursive least fixpoint — forward reachability. A fluent is reachable if it holds initially or is added by an applicable action; an action is applicable when none of its preconditions is unreachable. The universal “all preconditions reachable” is the standard double-negation encoding, because a forall may not sit inside a recursive cycle on this engine — the alternating fixpoint converges it:

pub derive unreached(a: Action) :- pre(a, f), not reachable(f);
pub derive applicable(a: Action) :- Action(a), not unreached(a);
pub derive reachable(f: Fluent) :- adds(a, f), applicable(a);

Arbitration — recursion through negation. Two conflicting actions cannot both run. scheduled recurses through its own negation via challenged, so {scheduled, challenged} form one NAF-cyclic SCC the engine evaluates by well-founded semantics directly (strict stratification would reject this):

pub derive challenged(a: Action) :- conflicts(a, b), scheduled(b);
pub derive scheduled(a: Action)  :- applicable(a), not challenged(a);

Running it

ox query enumerates every declared pub query. The plan chain closes over all seven fluents and all seven actions are applicable; the arbitration is the payoff:

query robot::reachableFluents:   7 row(s)
query robot::applicableActions:  7 row(s)
query robot::readyActions:       1 row(s)    — only `charge` (pre {atHome}, true at start)
query robot::scheduledActions:   4 row(s)    — {charge, navigate, scan, pickup}
query robot::challengedActions:  1 row(s)    — {pushObject}
query upper::involvement:        1 row(s)    — (pickup, rob): pickup exercises a capability rob bears

Two conflicts drive the arbitration. The asymmetric one resolves to a definite winner: pushObject is challenged by the higher-priority pickup, pickup has no rival so it is never challenged, so pickup is scheduled and pushObject is not. The symmetric one (wipeLeft ↔ wipeRight, no tiebreak) is well-founded-undefined: the engine materializes only definitely-true atoms, so neither appears in scheduled and neither appears in challenged — that absence-of-both is the deadlock’s observable signature.

Honest caveats (what runs today)

• ox query renders rows as opaque individual ids; the row counts and the named membership above are what the corpus test pins (it resolves the ids back to names).
• Arbitration is kept as a single SCC on purpose. Splitting it into a lower blocked stratum and a higher scheduled :- not blocked would ask the engine to read a well-founded relation under a higher negation — it materializes the WFS stratum two-valued at that boundary, so a genuinely-undefined atom would read as false downstream and over-assert. The single-SCC form is the sound one.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins scheduled = {charge, navigate, scan, pickup}, challenged = {pushObject}, and the absence of both symmetric-deadlock actions, so the well-founded arbitration can’t drift from the language.