This transformation is intended to address a source of inefficiency that we have noted which is a consequence of the manipulation that is required in order to make variables range over relations rather than domains. Consider example query ``what is Fred's age'':

The TRC translation of this query appears to have more existentially quantified variables than we might expect. The translation of DRC table membership clauses always results in extra existentially quantified variables in the TRC expression. This is unavoidable. However, if we look at the TRC query, we see that the existentially quantified variable, x, which also occurred in the DRC expression has now become redundant. Any attributes associated with this variable are equated with attributes of the new existentially quantified variable. We ought therefore to be able to eliminate this redundant variable. It actually turns out that every TRC existentially quantified variable which originated from a DRC existentially quantified variable is redundant and can be optimised away. We perform this optimisation by translating the TRC expression into clausal form and applying the paramodulation inference rule (which substitutes one term for another which is equal to it) until the redundant variables have been eliminated. (Details of the conversion to clausal form and the paramodulation inference rule may be found in [Bundy, 1983].) Converting the TRC expression above into clausal form produces the clause set:

For the purposes of this example, Skolem constants have been formed by
prefixing variable names with *sk*. We know that the variable
*x* is redundant, so we now select a clause which equates some
attribute of the Skolem constant associated with *x* to some
other value, and then substitute this other value for all occurrences
of the original. In the above example, if we choose the second clause
we know we can replace all occurrences of *skx.age* with
*skt.age*. Performing this substitution throughout reduces
the clause set to

There are no further clauses containing the redundant variable, so we have now finished. Reconstructing the formula produces the simplified TRC expression:

which is what we would expect.

With the query ``Who works in a department that is on floor 2?'' we obtain the following TRC, which is optimised as shown:

which reduces to the following clause set:

We know that we will be able to optimise away the variable *x*
(skolem constant *skx*), and we can do this by selecting the
second of these clause and substituting
for *skx.dept* throughout. This results in:

Reconstructing the TRC formula produces:

Chris Fox, September 1995