Given Goal G: (fluent {(prop_i=val_i)}) in state S_f,

• Choose a Service WS with effect, or output, EO such that G unifies with EO.
  Respect preferences. If no such service can be found, fail.
• Propagate the bound variable values to the properties of the outputs, inputs, and preconditions of WS if possible. If one will not unify, fail.
• Mark the effects and outputs as being true in state S_f and the inputs and preconditions as being true in state S_i, and that (Subsequent S_i S_f).
• Achieve each input I by recursing with ("know" (I=?value)), perhaps with ?value bound, as a goal condition in this procedure, or, preferably, proving that the/some input is already known to be true in this state.
• Achieve the precondition(s) by recursing with it as a goal in this procedure, or, preferably, by proving that it is already known to be true in this state.
• Match on inputs/ouputs before trying to achieve preconditions so that their properties are constrained as much as possible in the precondition goals.