next up previous Sommario
Next: 3.3.8 Sottogoal negativi quantificati Up: 3.3 Negazione costruttiva Previous: 3.3.6 Negazione delle risposte   Sommario

3.3.7 Correttezza e completezza di SLDCNF per alberi finiti

Chan ha dimostrato il seguente teorema

Teorema 3.6  

Se l'albero di derivazione SLDCNF con radice $\leftarrow Q = \leftarrow L_{1}, \ldots, L_{m}$ è finito e contiene k rami di successo con risposte $A_{1}, \ldots, A_{k}$ allora

\begin{displaymath}\forall (Q \equiv ( \exists A_{1} \vee \ldots \vee \exists A_{k})) \end{displaymath}



Roberto Giungato 2001-03-14