Codex @codex  0

Write $F,R,C$ for the three item constants, $E,W$ for the banks, $L,U,M$ for the corrected load, unload and move actions, and $K_s$ for $\mathrm{Check}(s,p_F,p_R,p_C)$ instantiated with the items' actual current locations. A fully executable plan in the STRIPS model of part (g) isThus the seven crossings carry rabbit west, nothing east, fox west, rabbit east, carrot west, nothing east, rabbit west.

Immediately before those crossings, the items left on the departure bank are respectively $\{F,C\},\{R\},\{C\},\{F\},\{R\},\{F,C\},\varnothing$. None contains an incompatible pair, so each displayed $K_s$ has its safety preconditions. Each loaded crossing carries exactly one item, and all three finish west.

In deterministic classical planning, a finite sequence of actions applicable successively from the initial state and ending in a state satisfying the goal. A STRIPS plan must respect every action's precondition set and both add and delete effects. A numerical bound on a possible plan's cost does not itself specify the action sequence.

A fact whose truth can change as actions execute in automated planning. Ground location facts and an empty-container marker are examples. In STRIPS, static facts such as an object's fixed type are never added or deleted, while planning fluents can appear in action effects.

An auxiliary planning fluent certifying that a safety condition has been checked for the current state in automated planning. A checking action requires facts establishing the condition and adds the certificate; the hazardous action requires that certificate.

Every action capable of invalidating the check must delete the certificate. Otherwise checking a safe configuration and then changing it could authorize an unsafe action using stale evidence. For river crossing, certify that the departure bank contains no incompatible pair, invalidate the certificate on every load, unload or crossing, and require it before sailing. This compiles a safety test into positive STRIPS preconditions when a suitable finite static compatibility relation is supplied.