6.2.2.3 Negazione costruttiva

Tale modulo sintetizza la negazione del sottoinsieme P1 del programma P, costituito delle clausole dei predicati che terminano sicuramente per goal non ground. Chiameremo comp(P1) il programma ottenuto.

Per ogni predicato $p_{h}$ di P1 si definisce in comp(P1) un predicato $\sim {p_{h}}$ nel seguente modo:

$$\sim {p_{h}} \leftarrow not \; p_{h}$$

Quando, durante il processo di derivazione, il sottogoal selezionato è del tipo not p, esso viene trattato con il metodo della negazione di Chan.

Vediamo ora un semplice

Esempio 6.6   Il predicato r è definito sui naturali.

$$r(s(0))\leftarrow$$

$$r(s(s(0)))\leftarrow$$

Poiché il criterio stabilisce che la query $\leftarrow r(x)$ termina,essendo ambedue le clausole fatti, il complemento di r è il seguente:

$$\sim{r}(x)\leftarrow not \; r(x)$$