quantifier elimination problem

From: Vadim Tropashko <Vadim_member_at_newsranger.com>
Date: Thu, 08 Mar 2001 03:28:32 GMT
Message-ID: <A%Cp6.870$54.953@www.newsranger.com>

I'm learning how quantifier elimination method from model theory works in relational database field. For example, formula

Exists i | Emp[i].name == 'Smith'

could be rewritten quantifier free as

Emp[ index('Smith') ].name == 'Smith'

As usual, additional function is required, and, not surprisingly, it is an index.

Now, how could I rewrite quantifier free the following formula

Forall i,j | (i==j or Emp[i].name!=Emp[j].name)

(this is unique key constraint:-) Can index function still be employed, or some new function (Eeek!) needs to be introduced?

Thank you for your time,
Vadim Received on Wed Mar 07 2001 - 21:28:32 CST