Укажите определение теоремы о достоверности отрицания по конечному неуспеху:
(Отметьте один правильный вариант ответа.)
Варианты ответа
пусть P — логическая программа без отрицаний. Если некоторое утверждение A имеет конечное дерево SLD-резолюции, заканчивающиеся неуспехом, то ![\[comp\left( P \right){\rm{ |= }}\neg {\rm{ }}A\]](https://intuit.ru//sites/default/files/tex_cache/7636f5d055bb45efc14ddb7ffa4d9d46.png)
(Верный ответ)
(Верный ответ)
пусть P — логическая программа без отрицаний. Если , то существует конечное дерево SLD-резолюции для A, заканчивающееся неуспехом
, то существует конечное дерево SLD-резолюции для A, заканчивающееся неуспехом
не выводимо тогда, когда A имеет конечное дерево вывода, заканчивающиеся неуспехом
