3.3.4 Derivazione

Sia $G_{k} = \leftarrow L_{1}, \ldots , L_{n}$ un goal e $L_{i}$ il letterale selezionato.

1. $L_{i}$ è il predicato di uguaglianza del tipo $r=s$. Se $r$ ed $s$ sono unificabili con mgu $\theta$ allora il goal derivato è $G_{k+1} = \leftarrow~(L_{1}, \ldots, L_{i-1}, L_{i+1}, \ldots, L_{n} ) \theta$.

2. $L_{i}$ è la disuguaglianza del tipo $r \neq s$ o $\forall (r \neq s)$. Se tale diseguaglianza è valida, allora il goal derivato è $G_{k+1} = \leftarrow L_{1}, \ldots, L_{i-1}, L_{i+1}, \ldots, L_{n}$.

   Se tale diseguaglianza è insoddisfacibile allora il goal $G_{k}$ fallisce.

   Si noti che le disuguaglianze soddisfacibili ma non valide non sono selezionate.

3. $L_{i}$ è un letterale positivo. Se c'è una clausola del programma $H \leftarrow~B_{1}, \ldots , B_{m}$ tale che esiste un mgu $\theta$ t.c. $L_{i} \theta = H \theta$ allora il goal derivato è $G_{k+1} = \leftarrow (L_{1}, \ldots, L_{i-1}, B_{1}, \ldots, B_{m}, L_{i+1}, \ldots, L_{n} ) \theta$.

4. $L_{i}$ è un letterale negativo della forma $\neg \exists Q$.

   Si calcolano le risposte a $\leftarrow Q$.

   • Se non esistono risposte a $\leftarrow~Q$ allora $G_{k+1}= \leftarrow~L_{1}, \ldots, L_{i-1}, L_{i+1}, \ldots, L_{n}$.

   • Se esistono $m$ risposte normalizzate $A_{1}, \ldots, A_{m}$ a $\leftarrow Q$ t.c. $\exists Q \equiv A_{1} \vee \ldots , \vee A_{m}$ allora
     
     $$\leftarrow L_{1}, \ldots, L_{i-1}, B_{j,1}, \ldots , B_{j,k_{j}}, L_{i+1}, \ldots, L_{n}$$
     
     
     dove $B_{j,1}, \ldots , B_{j,k_{j}}$ è la $NA_{j}$ in
     
     $$NA_{1} \vee \ldots \vee NA_{p} \equiv \neg (A_{1} \vee \ldots \vee A_{m})$$
     
     
     Se la risposta è equivalente a $true$, allora il goal $G_{k}$ fallisce.

Nelle sezioni successive esporremo il processo di normalizzazione delle risposte a $\leftarrow Q$. Vedremo quindi un procedura che permette di ottenere la negazione delle risposte stesse.

Una SLDCNF refutazione è una derivazione finita che termina

1. con la clausola vuota

2. con una clausola che contiene solo disuguaglianze primitive

L'ultimo caso è sempre un caso di terminazione con successo perché le diseguaglianze sono sempre soddisfacibili.