2.3 Risoluzione SLD

La semantica dei programmi logici può essere data seguendo due approcci equivalenti, quello dichiarativo, che vedremmo brevemente nelle sezione successiva, e quello procedurale che si basa sul metodo di risoluzione SLD.

Sia $G = A_{1}, \ldots ,A_{k}, \ldots ,A_{n}$ un goal e $C = A\leftarrow B_{1}, \ldots ,B_{q}$ una clausola del programma P. Se $A_{k}$ è l'atomo selezionato secondo la regola di selezione ed esiste $\theta$ mgu di $A_{k}$ ed A, il goal G' = $\leftarrow (A_{1}, \ldots ,A_{k-1}, B_{1}, \ldots ,B_{q},A_{k+1}, \ldots ,A_{k}) \theta$ è detto risolvente di G e C.

Una derivazione SLD di P$\cup${G} consiste di una sequenza (finita o infinita) $G_{0}=G$, $G_{1}, \ldots$ di goal, una sequenza di $C_{1},C_{2}, \ldots$ di varianti di clausole di P e una sequenza $\theta_{1}, \theta_{2}, \ldots$ di mgu tale che ogni $G_{i+1}$ è derivato da $G_{i}$ e $C_{i+1}$ usando $\theta_{i+1}$.

È indispensabile che ogni $C_{i}$ non contenga variabili già apparse nella derivazione fino a $G_{i-1}$: quindi è necessaria una fase di ridenominazione delle variabili.

Una refutazione SLD di P$\cup${G} è una derivazione SLD di P$\cup${G} che ha la clausola vuota $\Box$ come ultimo risolvente.

Una derivazione SLD è detta fallita se è finita e non è una refutazione.

Una sostituzione di risposta calcolata per $P \cup \{G\}$ è una sostituzione ottenuta restringendo la composizione $\theta_{1} \circ \ldots \circ \theta_{n}$ alle variabili di G, dove $\theta_{1}, \ldots, \theta_{n}$ e la sequenza di mgu usati in una refutazione SLD di P$\cup${G}.

Una regola di computazione è una funzione da un insieme di goal a un insieme di atomi che, dato un goal, restituisce un atomo di tale goal detto atomo selezionato.

Una derivazione (risp. refutazione) SLD via R è una derivazione (risp refutazione) SLD nella quale per selezionare gli atomi è sempre usata la regola R.

TEOREMA di indipendenza dalla regola di computazione

Se esiste una refutazione SLD di $P \cup \{G\}$ con risposta calcolata $\sigma$, allora per ogni regola di computazione R esiste una refutazione SLD di $P \cup \{G\}$ via R con risposta calcolata $\sigma '$ tale che $G\sigma '$ è una variante di $G\sigma$.

Sia P un programma e G un goal. Un albero SLD per $P \cup \{G\}$ è un albero che soddisfa le seguenti condizioni:

• ogni nodo dell'albero è un goal, eventualmente vuoto.
• la radice è G.
• sia $\leftarrow A_{1}, \ldots ,A_{m}, \ldots ,A_{k}$ un nodo dell'albero e $A_{m}$ sia l'atomo selezionato. Allora, per ogni clausola di input $A \leftarrow B_{1},\ldots ,B_{q}$ tale che $A_{m}$ e A sono unificabili con mgu $\theta$, il nodo ha un figlio
  
  $$\leftarrow (A_{1}, \ldots ,A_{m-1}, B_{1},\ldots ,B_{q}, A_{m+1}, \ldots ,A_{k}) \theta$$
  
  

• i nodi con clausola vuota non hanno figli.

Ogni ramo di un albero SLD è una derivazione di $P \cup \{G\}$. Rami corrispondenti a derivazioni infinite sono detti rami infiniti.

I sistemi PROLOG standard utilizzano la regola di computazione che seleziona sempre l'atomo più a sinistra (leftmost) insieme ad una regola di ricerca depth-first.