3.3 Negazione costruttiva

Nei paragrafi precedenti abbiamo visto quali sono i limiti di un sistema di programmazione logica che fa uso della regola di negazione come fallimento finito e come si cerchino altre tecniche per risolvere i problemi legati alla manipolazione di sottogoal negativi non necessariamente ground.

La Negazione costruttiva di Chan [Chan88,Chan89] si propone come una possibile soluzione a questo problema.

La NC sussume la regola di negazione come fallimento finito. Entrambe le regole hanno infatti come fondamento teorico la teoria del completamento di un programma logico, ma la NC formalizza un metodo per trattare sottogoal negativi non ground in termini della risoluzione SLDCNF che è un'estensione della risoluzione SLDNF.

Con la risoluzione SLDCNF i sottogoal negativi possono essere usati non solo come test ma anche per calcolare risposte come avviene per i sottogoal positivi; da qui il nome di negazione costruttiva.

L'idea di base è che la risposta ad un goal del tipo $\leftarrow \neg q$ è semplicemente la negazione della risposta di $\leftarrow q$. Come nella n.a.f. si fa uso dell'idea della subrefutazione ; infatti per valutare $\leftarrow \neg q$ si parte con una subrefutazione che ha come top query $\leftarrow q$.

Vedremo in seguito che è proprio questo il punto debole della NC, infatti se la valutazione della query $\leftarrow q$ dà luogo ad un albero di derivazione infinito, la procedura che andremo a esporre non può dare alcuna risposta al corrispondente sottogoal negativo.

Se la refutazione di $\leftarrow Q$ non coinvolge la selezione di alcun letterale negativo, detta $\theta$ una sostituzione di risposta calcolata e $X_{1}, \ldots , X_{n}$ sono le variabili in $\theta$, riferendoci alla teoria del completamento possiamo scrivere:

$$Q \leftarrow X_{1}=X_{1}\theta \wedge \ldots \wedge X_{n}=X_{n}\theta$$

se in $Q$ non ci sono variabili abbiamo $Q \leftarrow true$.

Se $A_{1}, \ldots ,A_{k}$ sono tutte le risposte alla query $\leftarrow Q$ possiamo scrivere, sempre per la teoria del completamento:

$$Q\equiv A_{1}\vee \ldots \vee A_{k}$$

Se non esistono risposte la parte destra è una disgiunzione vuota che è equivalente a $false$, e cioè permette di dedurre $\neg Q$. Se esiste una sola risposta $A_{1}$ equivalente a $true$, la parte destra è equivalente a $true$ e ciò vuol dire che possiamo dedurre che $\neg Q$ è falso. La regola di Negazione costruttiva a questo punto è semplicemente:

$$\neg Q \equiv \neg (A_{1}\vee \ldots \vee A_{k})$$

cioè la negazione delle risposte di $\leftarrow Q$ sono le risposte di $\leftarrow \neg Q$.

Tale regola può essere applicata anche quando la refutazione di $\leftarrow q$ coinvolge la selezione di letterali negativi.

A questo proposito vediamo i seguenti esempi:

Esempio 3.7  

$$p(a,1)\leftarrow$$

$$p(b, 2)\leftarrow$$

$$p(c, 3)\leftarrow$$

$$s(1)\leftarrow$$

$$m(x)\leftarrow p(x, y), s(y)$$

$$q(b, c)\leftarrow$$

$$q(a, y)\leftarrow h(x)$$

$$r(x)\leftarrow \neg m(x), q(x, y)$$

$$n(c,c)\leftarrow$$

$$n(b, x)\leftarrow g(x)$$

Consideriamo le query:

1. $\leftarrow \neg m(x)$

   $x = a$ è l'unica risposta a $\leftarrow m(x)$. Quindi possiamo concludere che $x \neq a$ è la risposta alla query $\leftarrow \neg m(x)$.

2. $\leftarrow m(x), q(x, y)$

   sotto il vincolo $x \neq a$ , la valutazione di $\leftarrow q(x, y)$ da la sola risposta $x = b$ $\wedge$ $y = c$.

3. $\leftarrow \neg r(x),s(x,y)$

   $\leftarrow r(x)$ ha successo con unica risposta $x=b$, ciò implica che $\leftarrow \neg r(x)$ ha risposta $x \neq b$. Ora la valutazione di $\leftarrow s(x,y)$ sotto il vincolo $x \neq b$ dà la risposta $x = b$, $y=c$.

Esempio 3.8  

Se il goal è $\leftarrow \neg p(x,y), q(x,y)$ e le due risposte a $\leftarrow \neg p(x,y)$ sono $x=a$, $y \neq b$ e $x=c$, $y \neq d$ abbiamo

$$p(x,y) \equiv (x=a \wedge y \neq b) \vee (x=c \wedge y\neq d)$$ (3.1)

usando la NC $\neg p(x,y)$ può essere sostituito dalla negazione della risposta di $p(x,y)$ e il goal derivato è:

$$\leftarrow ((x=a \wedge y\neq b) \vee (x=c \wedge y \neq d)), q(x,y)$$

Trattare questo goal è troppo complicato, allora si cerca di riportare il goal in una forma normale.

Lavorando sulla parte destra di 3.1 possiamo ottenere le seguenti formule per $\neg p(x,y)$

$$\neg p(x,y) \leftarrow x \neq a, x \neq c$$

$$\neg p(x,y) \leftarrow x =c, y=d$$

$$\neg p(x,y) \leftarrow x=a, y=b$$

Vedremo in seguito che la normalizzazione delle risposte non è sempre così immediata, per esempio nel caso in cui le risposte contengono funzioni e variabili.