3.3.1 Risoluzione SLDCNF

I sottogoal che sono trattati dalla NC sono del tipo

• $p(s_{1}, \ldots ,s_{n})$
• $\neg p(s_{1}, \ldots ,s_{n})$
• $s=t$
• $s \neq t$
• $\forall (s \neq t)$