6.1 Negazione intensionale e negazione costruttiva

La negazione intensionale, come visto in precedenza, sintetizza, a partire dalle definizioni di un predicato $p_{i}$, la definizione di un nuovo predicato $\sim p_{i}$ che può essere usato per calcolare l'insieme di fallimento finito di $p_{i}$.

La procedura di refutazione, dimostrata completa e corretta, ha il vantaggio, rispetto alla negazione come fallimento finito, di poter calcolare goal negativi non ground. D'altro canto, si è visto sperimentalmente che, sintetizzando $\sim p_{i}$, in alcuni casi il numero di clausole prodotte è eccessivamente elevato. Ciò è vero in particolare quando si trattano data base deduttivi, come si vede nel semplice esempio seguente:

Esempio 6.1  

Considerando la segnatura $\Sigma = \{ a_{1}, \ldots , a_{100} \}$, la negazione intensionale del fatto

$$p( a_{50} ) \leftarrow$$

dà luogo alle seguenti novantanove clausole:

$$\sim p(a_{1}) \leftarrow$$

$$\sim p(a_{49}) \leftarrow$$

$$\sim p(a_{51}) \leftarrow$$

$$\sim p(a_{100}) \leftarrow$$

La negazione costruttiva, come proposta da [Chan88], è una tecnica che permette di trattare goal aventi come sottogoal anche letterali negativi. È detta costruttiva perchè, a differenza della regola di negazione come fallimento finito, tali sottogoal possono essere trattati non solo come test, ma anche per calcolare valori.

Di tale tecnica è dimostrata la correttezza e la completezza solo per alberi di derivazione finiti; chiaramente, essendo basata sul calcolo e negazione delle risposte ai corrispondenti sottogoal positivi, si hanno problemi nel caso di alberi di derivazione infiniti.

La nostra proposta si prefigge di integrare i due metodi visti, cercando di ovviare ai difetti appena esposti. L'obbiettivo è, dato un programma P, sintetizzare per ogni predicato $p_{i}$ di P un nuovo predicato $\sim p_{i}$ inteso come il complemento di $p_{i}$, da usare quando nelle interrogazioni si vogliono calcolare valori per cui vale $\neg$ $p_{i}$.

Poichè in generale l'insieme complemento di $p_{i}$ è un insieme non effettivo, la definizione di $\sim p_{i}$ calcolerà la porzione computabile del complemento di $p_{i}$, ovvero il fallimento finito di $p_{i}$.