3.3.6 Negazione delle risposte

La negazione di una disgiunzione della forma $A_{1} \vee \ldots \vee A_{k}$ può essere ottenuta negando individualmente ogni $A_{i}$ $1 \leq i \leq k$ e ricombinando le componenti. Vedremo che la negazione di ogni $A_{i}$ non dà origine a nessun nuovo sottogoal.

La procedura ha bisogno di un'accurata trattazione della quantificazione implicita delle variabili quando la negazione della risposte coinvolge variabili.

La procedura è basata sulla seguente equivalenza che è vera per le uguaglianze ma non in generale:

$\exists x, y \neg \exists u (x = f(u), y = h(u)) \equiv \exists x, y \forall u (x \neq f(u)) \vee \exists x, y, u (x = f(u), u \neq h(u))$

Una risposta normalizzata è della forma

$$x_{1} = r_{1} \wedge \ldots \wedge x_{m} = r_{m} \wedge IE_{1} \wedge IE_{n}$$

Negando la parte di eguaglianze otteniamo le prime $m$ componenti

$$\forall y_{1}, \ldots , y_{nv_{1}} (x_{1} \neq r_{1})$$

$$x_{1} = r_{1}, \forall y_{n v_{1}+1}, \ldots ,y_{nv_{2}} (x_{2} \neq r_{2})$$

$$\vdots$$

$$x_{1} = r_{1}, \ldots , x_{m-1} = r_{m-1 }, \forall y_{nv_{m-1}+1} , \ldots , y_{nv_{m}} (x_{n} \neq r_{m})$$

dove $y_{1}, \ldots ,y_{nv_{1}}$ sono non-goal variabili in $x_{1} \neq r_{1}$, $y_{n v_{1}+1}, \ldots ,y_{nv_{2}}$ sono non-goal variabili in $x_{1} \neq r_{1}$ che non sono in $y_{1} \ldots y_{nv_{1}}$ etc.

Se $IE_{1}$ è $s_{1} \neq t_{1}$ allora la componente seguente è $x_{1} = r_{1} \wedge \ldots , x_{m} = r_{m} \wedge s_{1} = t_{1}$. Lo stesso se $IE_{1}$ è della forma $\forall (s_{1} = t_{1})$. Dopo la negazione, le variabili esplicitamente quantificate universalmente vengono implicitamente quantificate esistenzialmente.

I componenti successivi sono generati similmente.

Vediamo ora qualche esempio di negazione di risposte.

Esempio 3.10  

1. La negazione della risposta $x_{1} = a$ , $\forall u (x_{2} \neq f(u))$ dà la disgiunzione:
   
   $$i. \ x_{1} \neq a$$
   
   

   
   

   $$ii. \ x_{1} = a, x_{2} = f(u)$$
   
   

2. La negazione della risposta $x_{1} = f(u)$, $x_{2} = g(u)$, $u \neq 1$ dà la disgiunzione:

   
   

   $$i. \ \forall u (x_{1} \neq f(u))$$
   
   

   
   

   $$ii. \ x_{1} = f(u), x_{2} \neq g(u)$$
   
   

   
   

   $$iii. \ x_{1} = f(1), x_{2} = g(1)$$
   
   

3. La negazione della risposta $x_{1} = f(u, u, v)$, $x_{2} = g(v, w)$, $u \neq w$ dà la disgiunzione :

   
   

   $$i. \ \forall u, v (x_{1} \neq f(u, u, v))$$
   
   

   
   

   $$ii. \ x_{1} = f(u, u, v), \forall w (x_{2} \neq g(u, w))$$
   
   

   
   

   $$iii. \ x_{1} = f(u, u, v), x_{2} = g(v, u)$$
   
   

Considerando l'ultima disgiunzione come la negazione delle risposte a $p(x_{1},x_{2})$, si ha che il goal

$$\leftarrow \neg p(x_{1},x_{2}), q(x_{1},x_{2})$$

dà luogo a tre possibili goal derivati:

1. $\leftarrow \forall u,v \ (x_{1} \neq f(u,u,v)), q(x_{1},x_{2})$

2. $\leftarrow \forall w \ (x_{2} \neq g(v,w)), q(f(u,u,v), x_{2})$

3. $\leftarrow q(f(u,u,v), g(v,u))$