To match a list of literals against a list of ground literals
(e.g., a set of preconditions against a state description)
  and return the set of all substitutions that enable the match, 
 
  one may use a recursive algorithm 
    that maintains a list of substitutions found so far
    and attempts to extend them 
  such an algorithm would be invoked by 
    passing the two lists of literals, 
    together with an empty list of substitutions

One algorithm for extending solutions is:
  If the list of literals is empty, 
    return the substitutions found so far
  Otherwise find the list of substitutions
    that allow matching the first literal
    against some ground literal
  For each such substitution
    find recursively the substitutions that
      allow matching the rest of the literals
      against the list of ground literals
      after the new substitution is added to 
        the list of substitutions found so far 
    add all of these resulting substitutions to the output


So it's enough to know how to match a literal against a ground literal.
To do this, it is enough 
  to match the predicate names
    and the number of arguments
    and to match the argument lists
  and return the substitution that matches the argument lists


So it is enough to know how to match arguments lists.
Doing so requires only a simplified version
  of the algorithm presented earlier for unifying lists of terms
  since we may assume that the second argument list 
    is a list of object constants
So given a list of terms and a list of object constants,
  we may get a unifying substitution for them (if one exists) by
  
  Starting with an empty substitution
  Matching the next term against the next constant term
    if the next term in the first list is a constant, then
      failing if the terms fail to match, and 
      continuing if the terms match
    otherwise (since one term is a variable)
      creating a binding of the variable term to the constant term
      adding this binding to the output
      continuing with 
        the result of applying this new binding
          to the rest of the first list of terms, and
        the rest of the second list of terms


Note that application of any substitution found by these algorithms is
straightforward, since no binding involves more than one variable, and
thus bindings needn't be composed.