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 — plus a fourth regime: federating a precondition across two disagreeing sensor standpoints, where the conflict surfaces as the four-valuedboth. Also: an upper ontology is an ordinary module, not a language built-in. Prerequisites: first-class relations;deriverule bodies; negation-as-failure. For the sensor federation: federation disagreement. 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);
Federating a precondition across disagreeing sensors — the four-valued both. The planner reads the initial state from a single trusted holds(f) extent. Real robots read the world from sensors, and sensors disagree. sensors.ar models two — lidar and camera — as standpoints over the planner’s own holds relation. A federated query joins them by the four-valued information-join (is/not/can/both); a pub fact asserts a fluent in that sensor’s view, a pub not_fact positively refutes it (RFD 0010 strong negation, not silence):
use robot::{ Fluent, holds };
pub standpoint lidar;
pub standpoint camera;
pub standpoint lidar { pub fact holds(clearPath); pub not_fact holds(objectVisible); }
pub standpoint camera { pub not_fact holds(clearPath); pub fact holds(nearObject); }
pub query sensedState() -> holds across [lidar, camera];
The decisive row is clearPath → Both: lidar asserts the path is clear, camera refutes it, and the information-join carries both polarities rather than picking a winner or crashing. clearPath is the precondition for navigate, so the federation tells the planner — as a value — that its sensors are in conflict about whether it may proceed.
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 sensors::sensedState: 4 row(s) — clearPath → Both, nearObject → Is, objectVisible → Not
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 queryrenders 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
blockedstratum and a higherscheduled :- not blockedwould 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}, the absence of both symmetric-deadlock actions, and the sensor federation’s per-fluent Truth4 verdicts (clearPath → Both, nearObject → Is, objectVisible → Not), so the well-founded arbitration and the four-valued information-join can’t drift from the language.
Source
The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.
root.ar
//! # Robot plan execution — WFS arbitration over a self-defined upper ontology
//!
//! A two-module package modeling a mobile robot that executes a plan. The split
//! is deliberate and load-bearing:
//!
//! * `upper` — a minimal upper ontology defined *in this package* (`Object`,
//! `Event`, `Capability`, `bears`, `exercises`, derived `involves`). Argon
//! is ontology-neutral; the foundational categories are an ordinary module,
//! not a language built-in — a published foundational ontology could be
//! imported in its place without touching the domain.
//!
//! * `robot` — the domain. It `use`s `upper`, specialises its categories
//! (`Agent <: Object`, `Action <: Event`, `Skill <: Capability`), and
//! builds a plan executor with three reasoning regimes: a bounded universal
//! (`applicable`), a positive least fixpoint (`reachable`), and arbitration
//! by **recursion through negation** (`scheduled` recurses through its own
//! negation via `challenged` — one well-founded SCC, queried directly).
//!
//! See `robot.ar` for the scenario and the precise modeling of the asymmetric
//! (resolving) and symmetric (deadlock) conflicts.
mod upper;
mod robot;
mod sensors;
robot.ar
//! # `robot` — plan execution for a mobile robot, over the `upper` vocabulary
//!
//! This module `use`s the package's own upper ontology and *specialises* it for
//! a robotics domain: an `Agent` is an `Object`, an `Action` is an `Event`, a
//! `Skill` is a `Capability`. The cross-module dependency is real — these
//! subkind declarations resolve their supertypes in the sibling `upper` module,
//! and the two files elaborate into one artifact.
//!
//! On top of the imported vocabulary it builds a small **plan executor** that
//! exhibits three reasoning regimes, each a workhorse of knowledge
//! representation:
//!
//! 1. **The bounded universal `forall`** (`readyAtStart`). An action is
//! ready-at-start when **every** one of its preconditions holds in the
//! initial state. This is the *true* universal — lowered to a
//! count-equality, never the existential "some precondition holds".
//!
//! 2. **A least fixpoint** (`reachable` / `applicable`). A fluent is reachable
//! if it holds initially, or if some applicable action adds it; an action
//! is applicable when none of its preconditions is unreachable. The two
//! relations are mutually recursive — the executor walks the plan forward
//! to its closure (charge → navigate → scan → pick up). The universal
//! "all preconditions reachable" is expressed by *double negation*
//! (`applicable` = not (`unreached`)), the standard Datalog encoding of a
//! universal that recurses; the alternating-fixpoint engine converges it.
//!
//! 3. **Recursion through negation** (`scheduled` / `challenged`). Two actions
//! that conflict cannot both run. `scheduled(a)` holds when `a` is
//! applicable and **not** challenged; `challenged(a)` holds when a
//! conflicting `b` is itself scheduled. So `scheduled` recurses through its
//! own negation *via* `challenged` — exactly the win–move game on the
//! conflict graph — and `{scheduled, challenged}` form ONE NAF-cyclic SCC
//! the engine evaluates by **well-founded semantics** (strict
//! stratification rejects a rule that recurs through its own negation).
//! An asymmetric (prioritised) conflict resolves to a definite winner; a
//! symmetric conflict is a genuine standoff whose well-founded value is
//! *undefined* — observable as the **absence of both** actions from the
//! `scheduled` extent (and from `challenged`).
use upper::{ kind, Object, Event, Capability };
// ── Domain specialisation of the upper-ontology categories ──────────────────
/// A robot — an object that bears skills and performs actions.
pub kind Agent <: Object;
/// A plan step — an event the agent can perform.
pub kind Action <: Event;
/// A capability the agent bears (grasping, locomotion, …).
pub kind Skill <: Capability;
/// A propositional state of the world the planner tracks (battery charged,
/// path clear, object visible, …). Fluents are the planner's currency.
pub kind Fluent {}
// ── Planner relations (asserted as the scenario ABox below) ─────────────────
/// `pre(a, f)` — action `a` requires fluent `f` to hold before it can run.
pub rel pre(a: Action, f: Fluent);
/// `adds(a, f)` — running action `a` makes fluent `f` hold (its effect).
pub rel adds(a: Action, f: Fluent);
/// `holds(f)` — fluent `f` is true in the initial state (a base fact).
pub rel holds(mut f: Fluent);
/// `conflicts(a, b)` — action `a` is challenged by action `b`: they cannot both
/// be scheduled. Read directionally for the arbitration game below.
pub rel conflicts(a: Action, b: Action);
// ── 1. The true universal: readiness in the initial state ───────────────────
/// `readyAtStart(a)` — **every** precondition of `a` holds in the initial
/// state. The `forall` ranges over the action's preconditions; an action with
/// a precondition that does not initially hold is excluded. This is a genuine
/// universal — lowered to `#{f : pre(a,f), holds(f)} == #{f : pre(a,f)}` — 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);
// ── 2. The least fixpoint: forward reachability ─────────────────────────────
//
// `applicable` quantifies universally over preconditions ("none unreachable"),
// `reachable` feeds back into `applicable` — a mutually recursive fixpoint.
// The universal is written as double negation because a `forall`/aggregate may
// not appear *inside* a recursive cycle on this engine (it is evaluated as a
// strict, lower-stratum dependency); the `not unreached` form is the standard
// Datalog encoding of the recursive universal, and the alternating fixpoint
// converges it.
/// `unreached(a)` — `a` has at least one precondition that is not (yet)
/// reachable. The existential witness of a *failed* universal.
pub derive unreached(a: Action) :- pre(a, f), not reachable(f);
/// `applicable(a)` — `a` is applicable when none of its preconditions is
/// unreachable, i.e. *all* are reachable (the universal, by double negation).
pub derive applicable(a: Action) :- Action(a), not unreached(a);
/// A fluent that holds initially is reachable (base case).
pub derive reachable(f: Fluent) :- holds(f);
/// A fluent added by an applicable action is reachable (recursive case). Mutual
/// recursion with `applicable` drives the plan forward to its closure.
pub derive reachable(f: Fluent) :- adds(a, f), applicable(a);
// ── 3. Arbitration: recursion through negation (well-founded semantics) ─────
//
// Arbitration is ONE recursion-through-negation SCC, queried directly. We do
// NOT split it into a lower `blocked` stratum and a higher `scheduled :- not
// blocked` stratum: that split asks the engine to read a well-founded relation
// under a *higher* negation, and the engine materializes the WFS stratum
// 2-valued at the boundary, so a genuinely-undefined atom would read as false
// downstream and over-assert. Instead `scheduled` recurses through its own
// negation **via** `challenged`, so `{scheduled, challenged}` form a single
// NAF-cyclic SCC the engine evaluates by well-founded semantics directly.
/// `challenged(a)` — `a` is challenged when some action `b` that conflicts with
/// it is itself `scheduled`. This is one half of the win–move game on the
/// conflict graph; the other half is `scheduled`, which negates `challenged`.
// ANCHOR: wfs
pub derive challenged(a: Action) :- conflicts(a, b), scheduled(b);
/// `scheduled(a)` — `a` runs if it is applicable and **not** challenged.
///
/// `scheduled` recurses through its own negation via `challenged`
/// (`scheduled` → `not challenged` → `scheduled`), so `{scheduled, challenged}`
/// is a single SCC the engine evaluates by well-founded semantics — no higher
/// stratum negates a WFS relation, so the model is sound:
///
/// * An ASYMMETRIC (prioritised) conflict resolves to a **definite winner**:
/// the uncontested action is scheduled, and its rival is challenged and so
/// absent from `scheduled`.
/// * A SYMMETRIC conflict is well-founded-**undefined**: the engine
/// materializes only definitely-true atoms, so neither side is scheduled
/// and neither side is challenged. The deadlock's observable signature is
/// the **absence of both actions from `scheduled`** (and from `challenged`).
pub derive scheduled(a: Action) :- applicable(a), not challenged(a);
// ANCHOR_END: wfs
// ── Scenario ABox ───────────────────────────────────────────────────────────
//
// The fluents:
// atHome, clearPath — true initially (holds)
// haveBattery — added by `charge`
// nearObject — added by `navigate`
// objectVisible — added by `scan`
// holding — added by `pickup` / `pushObject`
// wiped — added by either wipe action
//
// The plan chain (each action's preconditions are the previous effects):
// charge : pre {atHome} adds {haveBattery}
// navigate : pre {haveBattery, clearPath} adds {nearObject}
// scan : pre {nearObject} adds {objectVisible}
// pickup : pre {objectVisible, haveBattery} adds {holding}
//
// So reachability closes over all seven fluents (atHome, clearPath,
// haveBattery, nearObject, objectVisible, holding, wiped) and all seven
// actions are applicable.
//
// Two conflicts exercise the well-founded arbitration:
//
// ASYMMETRIC (resolves): `pickup` and `pushObject` contend for the manipulator.
// `pushObject` is the lower-priority fallback, so it is *challenged by*
// `pickup`: conflicts(pushObject, pickup). `pickup` has no conflicting
// rival, so it is never challenged ⇒ pickup is scheduled; hence pushObject is
// challenged (its rival pickup is scheduled) ⇒ pushObject is NOT scheduled.
// (pushObject is itself applicable — pre {nearObject} — so arbitration, not
// inapplicability, is what stops it.) A definite winner: pickup.
//
// SYMMETRIC (deadlock): `wipeLeft` and `wipeRight` mutually conflict with no
// tiebreak: conflicts(wipeLeft, wipeRight) and conflicts(wipeRight, wipeLeft).
// Each is applicable (pre {haveBattery}). Their scheduled/challenged-values
// form a 2-cycle through negation, so both are well-founded-*undefined*:
// neither appears in `scheduled`, and neither appears in `challenged`.
pub fact Fluent(atHome)
pub fact Fluent(clearPath)
pub fact Fluent(haveBattery)
pub fact Fluent(nearObject)
pub fact Fluent(objectVisible)
pub fact Fluent(holding)
pub fact Fluent(wiped)
pub fact Action(charge)
pub fact Action(navigate)
pub fact Action(scan)
pub fact Action(pickup)
pub fact Action(pushObject)
pub fact Action(wipeLeft)
pub fact Action(wipeRight)
// Initial state.
pub fact holds(atHome)
pub fact holds(clearPath)
// Preconditions.
pub fact pre(charge, atHome)
pub fact pre(navigate, haveBattery)
pub fact pre(navigate, clearPath)
pub fact pre(scan, nearObject)
pub fact pre(pickup, objectVisible)
pub fact pre(pickup, haveBattery)
pub fact pre(pushObject, nearObject)
pub fact pre(wipeLeft, haveBattery)
pub fact pre(wipeRight, haveBattery)
// Effects.
pub fact adds(charge, haveBattery)
pub fact adds(navigate, nearObject)
pub fact adds(scan, objectVisible)
pub fact adds(pickup, holding)
pub fact adds(pushObject, holding)
pub fact adds(wipeLeft, wiped)
pub fact adds(wipeRight, wiped)
// Asymmetric conflict: pushObject is challenged by the higher-priority pickup.
pub fact conflicts(pushObject, pickup)
// Symmetric conflict: wipeLeft and wipeRight deadlock.
pub fact conflicts(wipeLeft, wipeRight)
pub fact conflicts(wipeRight, wipeLeft)
// ── Queries ─────────────────────────────────────────────────────────────────
/// Actions all of whose preconditions hold in the initial state (true forall).
pub query readyActions() -> readyAtStart;
/// Fluents reachable from the initial state by the applicable plan.
pub query reachableFluents() -> reachable;
/// Actions all of whose preconditions are reachable.
pub query applicableActions() -> applicable;
/// Actions challenged by a scheduled rival (well-founded; the win–move dual of
/// `scheduled`).
pub query challengedActions() -> challenged;
/// Actions that actually run: applicable and unchallenged.
pub query scheduledActions() -> scheduled;
upper.ar
//! # `upper` — a small upper ontology, defined in this package
//!
//! Argon is ontology-neutral: the foundational categories a domain reasons
//! over come from an ordinary module, not from the language. This package
//! defines its own minimal upper ontology — three categories and two
//! relations are enough for the planner. A published foundational ontology
//! (UFO, BFO) could be imported in its place and the domain module would not
//! change.
//!
//! The one derived relation is the point of the module: an event *involves*
//! an object exactly when the event exercises a capability the object bears.
//! Involvement is never asserted directly; it is derived.
// Vocabulary (§3.4, §5.2): a concept introducer must resolve to a visible
// `pub metatype` that is IN SCOPE — declared locally or imported (RFD 0038
// D4; the baseline `type`/`rel` come from this package's
// `[package].prelude = ["std::core::{type, rel}"]`). This upper ontology
// declares the one classifier it commits to — `kind`, a rigid sortal — and
// the domain module (`robot`) imports it (`use upper::{kind, …}`) to
// classify its own `pub kind` declarations.
/// Kind: a rigid sortal classifier supplying an identity principle.
pub metatype kind = { };
/// A thing that persists through time and bears capabilities.
pub kind Object {}
/// An occurrence.
pub kind Event {}
/// A power an object bears, exercised by events.
pub kind Capability {}
/// `bears(o, c)` — object `o` bears capability `c`.
pub rel bears(o: Object, c: Capability);
/// `exercises(v, c)` — event `v` exercises capability `c`.
pub rel exercises(v: Event, c: Capability);
/// `involves(v, o)` — event `v` involves object `o`: it exercises a
/// capability `o` bears. Derived, never asserted.
pub derive involves(v: Event, o: Object) :- bears(o, c), exercises(v, c);
// A minimal self-contained instance so the derived relation is observable
// on its own: `rob` bears `grasping`; the `pickup` event exercises it.
pub fact Object(rob)
pub fact Capability(grasping)
pub fact Event(pickup)
pub fact bears(rob, grasping)
pub fact exercises(pickup, grasping)
/// The involvement extent — `(event, object)` pairs.
pub query involvement() -> involves;
sensors.ar
//! # `sensors` — federating a precondition across two disagreeing sensors
//!
//! The planner in `robot.ar` reads the initial state from a single, trusted
//! `holds(f)` extent. Real robots don't have one: the world is reported by
//! *sensors*, and sensors disagree. A LiDAR sweep may report the path clear
//! while the camera, seeing glare, reports it blocked. A planner that picks one
//! sensor and ignores the other is silently unsound; one that crashes on the
//! conflict is useless. Argon does neither — it federates the two readings and
//! reports the disagreement **as a value**.
//!
//! Each sensor is a `standpoint`: its own source of ground truth over the SAME
//! `holds` relation the planner reads. A sensor `pub fact holds(f)` asserts the
//! fluent; a `pub not_fact holds(f)` is a positive refutation (RFD 0010 strong
//! negation), not mere silence. A federated query joins the sensors by the
//! four-valued information-join over the Belnap-Dunn bilattice (`Truth4`):
//!
//! * `is` — asserted by some sensor, refuted by none
//! * `not` — refuted by some sensor, asserted by none
//! * `can` — neither (a fluent no sensor mentions)
//! * `both` — asserted by one sensor AND refuted by another: the conflict,
//! carried rather than discarded
//!
//! The scenario, over the planner's own fluents:
//!
//! clearPath — lidar asserts `holds`, camera refutes it → Both
//! nearObject — only the camera reports it (lidar silent) → Is
//! objectVisible — only the lidar refutes it (camera silent) → Not
//! atHome — asserted only in the base both sensors inherit → Is
//!
//! `both` is the load-bearing row: `clearPath` is the precondition for
//! `navigate`, and the federation tells the planner — without crashing and
//! without silently picking a winner — that its sensors are in conflict about
//! whether the path is clear.
//!
//! Soundness: `Argon.Standpoint.Federation.federate_eq_both_iff` (Lean, proven)
//! — the per-row `Truth4` the federated dispatcher computes is exactly the AFT
//! info-join across the contributing standpoints.
use robot::{ Fluent, holds };
// Each sensor is a source of ground truth — a standpoint over `holds`.
pub standpoint lidar;
pub standpoint camera;
pub standpoint lidar {
// LiDAR sweeps the floor: it reads the path as clear.
pub fact holds(clearPath);
// It cannot see the object yet (occlusion) — a positive refutation.
pub not_fact holds(objectVisible);
}
pub standpoint camera {
// The camera, against glare, reads the path as blocked — refuting `clearPath`.
pub not_fact holds(clearPath);
// It does see the object in frame.
pub fact holds(nearObject);
}
// Federate the two sensors' readings of `holds`. Each standpoint also inherits
// the base `holds` extent (robot.ar asserts `holds(clearPath)` and
// `holds(atHome)`) as a global section, so the query returns one row per fluent
// any source speaks to, each tagged with the joined four-valued status.
// `clearPath` is asserted by the base and by `lidar` and refuted by `camera`, so
// the information-join carries both polarities: `Both` — the camera's refutation
// surfaces even against the base assertion. `atHome`, asserted only in the base
// that both sensors inherit, comes back `Is`.
pub query sensedState() -> holds across [lidar, camera];