This page describes a basic (and sometimes inaccurate) way of stripping structures from predicates. We can strip argument N from the definition of a target predicate named P by performing, in the order given, the following transformations to each of its clauses:
to 
.
to 
, where V is a new
variable not appearing in the clause.
We can match a skeletal definition with the definition generated by stripping an argument from a target predicate if for every clause in the skeletal definition there is a corresponding clause in the stripped definition such that the clauses match, and no two clauses in the skeletal clause are matched to the same clause in the stripped definition. Two clauses match if:
and 
predicates of book Chapter 6)
then we remove a sequence of one or more unit goals from the
stripped clause.
is not allowed to match
with a target term 
, since this would instantiate X to
. However, the match is permitted is the skeletal term is
and the target term is 
.
Let us apply this method to the example we gave in
Chapter 6 of the book. This time we assume that our ``case library''
is simply a file of predicate definitions, of which one is the
satisfy predicate defined at 
. Suppose that, in our
techniques editor, we have selected the recursive deconstruction skeleton
and have instantiated it in a similar way to an
early stage of the example at 
(although without
committing to the predicate name, which we leave as the variable,
P). Our skeleton is:
We now want to find whether there is an existing predicate definition which might be relevant to this skeleton so we apply our method for stripping arguments to our definition of satisfy. This yields five sets of clauses (one for each argument in satisfy), which we give below, in the order of the argument position from which they were stripped.
If we now apply our matching method to these five candidates we obtain
only one match, which is between the skeleton and
candidate 1. The correspondence of unit goals in this
match is shown in the table below, where the first column gives the
number of the clauses which match
, the second column shows the matching term in
the skeleton and the third column shows the matching term in the
target.
None of the other candidates match. There are various reasons why
each could be rejected but the most immediate one is that none of the
heads of clauses in the other candidates can be unified with the head
of the second clause of the skeleton without binding a variable in the
candidate to a term from the skeleton. For instance, the head of every
clause in candidate 2 is 
and if we unify
this with 
then the variable D is bound to the term
, which contravenes the restriction on unification
placed on our matching method.
You may have noticed that the single match we obtained (candidate 1) is exactly the predicate which we obtained in Chapter 6 of the book by undoing some of the additions made when constructing the original definition of satisfy by techniques editing. Therefore, we could complete our current example by taking candidate 2 and adapting it as shown in the book.
