Re: quantifier elimination problem

Hi,

Vadim Tropashko schrieb:
> 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.

in program implementations of predicate logic theorem solvers you can usually omit the all-quantifier, and all variables are considered all-quantified implicitly. Instead of "(forall ?x (red ?x))" to express any object is red, you can write "(red ?x1)". Note that new variables are introduced for each quantifier expression.

Existence-quantifiers are simplified by a so called Skolem function. To express there is a green object "(exists ?x (green ?x))" write "(green (f1 ?x2))", where f1 is a new function symbol and ?x2 a new variable.

> 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?

I suppose your function index(x) yields one (of possibly many) row number if there is a record which has at least one field in it with a content x, and a pointer to an empty row, if there is no such record.

You could at least lower the complexity of the statement:

Forall i | Emp[i].name = Emp[index(Emp[i].name)]

Greetings,
Joachim Received on Thu Mar 08 2001 - 11:03:53 CET