6.3 Negazione di $P$ $=$ $< P^{+} , P^{-}>$

In questa sezione viene esposto un teorema che permette, dato un programma già rappresentato come una coppia, di calcolarne il complementare attraverso una trasformazione sintattica, senza ripercorrere i passi visti.

Teorema 6.4  

Dato il programma $P$ rappresentato come la coppia $< P^{+} , P^{-}>$

$$Not(P) = <P^{-} , P^{+}>_{[p/ \sim p, \sim p / p]_{p \in \Pi}}$$

dim.

Valendo, secondo [MPRT90], un risultato analogo quando l'operatore $Not$ realizza solo la negazione intesionale, è sufficiente dimostrare che la relazione vale sul programma costituito dai predicati, e dalle relative clausole, che il criterio ha stabilito non terminare.

Si considerino quindi le clausole del tipo

$$\sim p(x) \leftarrow not \ \ p(x)$$

ottenute dal processo di negazione costruttiva. Poiché $\leftarrow p(x)$ termina e l'unica clausola che definisce $\sim p$ è quella appena vista, anche $\leftarrow \sim p(x)$ termina. Quindi applicando la negazione costruttiva e assumendo che $\sim \sim p$ $=$ $p$, si ottiene la clausola che definisce $p$:

$$p(x) \leftarrow not \ \ \sim p(x)$$

Tale clausola corrisponde a quella ottenuta secondo la trasformazione sintattica.

Poiché il programma finale si ottiene con l'unione dei complementari delle due partizioni, la relazione vale.

$\quad\Box$