  In logic programming, the sort of reasoning required to resolve (51) is carried out by a derivation procedure called resolution. We will use resolution here in a non-standard way, i.e. logic programming combined with integrity constraints (for details see van Lambalgen and Hamm 2005). It starts with the formula that has to be made true in the discourse model. Resolution proceeds by identifying rules which have the query as their consequent and substituting the consequent with the antecedent conditions of the rule, making the antecedent formulas new queries themselves. The resolution stops when the query cannot be further resolved, that is, when a plan has been computed whose preconditions are all fulfilled given an appropriate update of the discourse model. To get an impression of how this works we will illustrate the resolution of (51). First, we have to compute the completion of the program and whenever possible substitute the variables with constants, in our case Loaded and  now. In logic programming this substitution is done automatically via unification. Here is the completion of the HoldsAt predicate which forms the head of two axioms—(35) and (36). 