A resolução está completa ou apenas a refutação concluída?

Passando por alguns tutoriais de representação do conhecimento sobre resolução no momento, deparei-me com o slide 05.KR, no77 .

Lá é mencionado que "o procedimento também está completo".

Eu acho que essa completude não pode significar que, se uma sentença for envolvida por KB, ela será derivada por resolução. Por exemplo, a resolução não pode derivar de um KB com cláusula única . (Exemplo de KRR, Brachman e Levesque, página 53).$(q \lor \neg q)$$\neg p$

Alguém poderia me ajudar a descobrir o que se entende neste slide? A integridade do slide refere-se a um procedimento de refutação completo e não a um procedimento completo de prova?

A resolução está completa como um sistema de refutação. Ou seja, se$S$ é um conjunto contraditório de cláusulas, a resolução pode refutar $S$, ie $S \vdash \bot$.

Isso é suficiente, pois $T \vdash A$ é equivalente a $T \cup \{\lnot A\} \vdash \bot$. Então, se queremos ver uma fórmula$A$ é derivável de $T$, precisamos apenas verificar se há uma prova de refutação para $T \cup \{\lnot A\}$ que pode ser verificado usando a resolução.

A resolução é apenas refutacionalmente concluída, como você mencionou. Isso é pretendido e muito útil, porque reduz drasticamente o espaço de pesquisa. Em vez de ter que derivar todas as conseqüências possíveis (para encontrar uma prova de alguma conjectura), a resolução está apenas tentando derivar a cláusula vazia.

Também é implicacionalmente completo no seguinte sentido:

Se um conjunto de cláusulas $F$ implica uma cláusula não tautológica $C$, sempre é possível derivar uma única cláusula $C'$ que inclui $C$ (ie $C' \subseteq C$)

Fonte:
Christian G. Fermüller, Conclusão implícita da resolução assinada, 2002

Observe que o resultado original é referido em:
RCT Lee. Um teorema de completude e um programa de computador para encontrar teoremas derivados de axiomas dados. Ph.D. Tese, Universidade da Califórnia, Berkely, 1967.