2.4.1 Modelli di Herbrand e operatore $T_{P}$

Sia L un linguaggio del primo ordine il cui insieme di costanti è non vuoto. L'universo di Herbrand $U_{L}$ per L è l'insieme di tutti i termini ground di L. La base di Herbrand $B_{L}$ per L è invece definita come l'insieme di tutti gli atomi ground di L. Una interpretazione di Herbrand per L è un'interpretazione tale che:

• il suo dominio è l'universo di Herbrand.
• ogni costante in L è assegnata a se stessa.
• se f è una funzione n-aria in L, allora è assegnata alla funzione $f_{I}$ da $(U_{L})^{n}$ ad $U_{L}$ definita assegnando il termine ground $f(t_{1},\ldots ,t_{n})$ alla sequenza $t_{1},\ldots ,t_{n}$ di termini ground.

Un modello di Herbrand per un insieme di formule S è un'interpretazione di Herbrand per S che sia anche un modello.

Per caratterizzare i modelli di programmi logici, introduciamo l'operatore di conseguenza immediata $T_{P}$ che trasforma interpretazioni di Herbrand in interpretazioni di Herbrand. Dato un programma P ed un'interpretazione I, poniamo

$$A \in T_{P}(I)$$

se solo se esistono degli atomi $B_{1},\ldots ,B_{n}$ tali che $A \leftarrow B_{1},\ldots ,B_{n} \in {\em ground(P)}$ e $I\models B_{1}\wedge ,\ldots ,\wedge B_{n}$

Alternativamente, per un atomo ground A

$$A \in T_{P}(I)$$

se e solo se esistono una sostituzione $\theta$ ed una clausola $B\leftarrow B_{1},\ldots ,B_{n}$ tali che $A\equiv B\theta$ e $I\models (B_{1}\wedge ,\ldots ,\wedge B_{n})\theta$.

Elenchiamo ora alcuni risultati fondamentali.

TEOREMA (correttezza della derivazione SLD)

Sia P un programma e $G= \leftarrow A_{1},\ldots ,A_{k}$ un goal. Supponiamo che esista una refutazione SLD di $P\cup \{G\}$ con sequenza di sostituzioni $\theta _{0},\ldots ,\theta _{n}$. Allora $(A_{1}\wedge \ldots \wedge A_{k})\theta _{0}\circ \ldots \circ \theta _{n}$ è una conseguenza semantica di P.

COROLLARIO

Se esiste una refutazione SLD di $P\cup \{G\}$ allora $P\cup \{G\}$ è inconsistente.

LEMMA

Sia S un insieme di universali. Se S ha un modello allora ha un modello di Herbrand.

TEOREMA (di Caratterizzazione)

Sia P un programma. Allora P ha un modello di Herbrand $M_{P}$ che soddisfa le seguenti proprietà:

• $M_{P}$ è un modello minimo di P.
• $M_{P}$ è il minimo fixpoint di $T_{P}$.
• $M_{P}$= $T_{P}\uparrow \omega$.

COROLLARIO

L'insieme di successo di un programma P è contenuto nel suo modello minimo di Herbrand.

Sia P un programma e $G = \leftarrow A_{1},\ldots ,A_{n}$ un goal. Diciamo che $\theta$ è una sostituzione di risposta corretta per $P\cup \{G\}$ se $\theta$ opera solo su variabili presenti in G e vale $P\models (A_{1}\wedge \ldots \wedge A_{n})\theta$.

TEOREMA

Sia P un programma e G un goal. Per ogni sostituzione di risposta corretta $\theta$ per $P\cup \{G\}$ esiste una sostituzione di risposta calcolata $\sigma$ per $P\cup \{G\}$ tale che $G\sigma$ è più generale di $G\theta$.

TEOREMA (Forte Completezza della derivazione SLD)

Dato un programma P ed un goal G, supponiamo che $P\cup \{G\}$ sia inconsistente. Allora ogni albero di derivazione SLD con radice G è di successo.

TEOREMA (di Successo)

Dato un programma P ed un atomo ground A, i seguenti fatti sono equivalenti:

• A è nell'insieme di successo di P.
• $A\in T_{P} \uparrow \omega$.
• ogni albero di derivazione SLD con radice $\leftarrow A$ è di successo.
• $P \models A$.