Завершено резолюция или только опровержение?

Question

Проходя через Некоторые учебники по представлению знаний по резолюции на данный момент, и я наткнулся Слайд 05.kr, №77.

Там упоминается, что «процедура также завершена».

Я думаю, что эта полнота не может означать, что если KB повлечет за собой предложение, то оно будет получено в результате разрешения. Например, разрешение не может получить $ (q lor neg q) $ из Kb с единственным пунктом $ neg p $. (Пример из KRR, Brachman и Levesque, стр. 53).

Может ли кто -нибудь помочь мне понять, что подразумевается на этом слайде? Является ли полнота слайда, ссылаться на то, чтобы быть выполненным опровержением, а не полной процедурой доказательства?

Answer 1

Разрешение завершено как система опровержения. То есть, если $ s $ является противоречивым набором пунктов, то разрешение может опровергнуть $ s $, то есть $ s vdash bot $.

Этого достаточно, так как $ t vdash a $ эквивалентно $ t cup { lnot a } vdash bot $. Поэтому, если мы хотим, чтобы формула $ a $ можно получить от $ t $, нам нужно только проверить, есть ли доказательство опровержения для $ t cup { lnot a } $, которые можно проверить с помощью разрешения.

Answer 2

Резолюция только опровергает, как вы упомянули. Это намеревался И очень полезно, потому что он резко уменьшает пространство поиска. Вместо того, чтобы в конечном итоге получить все возможные последствия (чтобы найти доказательство какой -либо предположения), разрешение только пытается получить пустой предложение.

Answer 3

Это также имеет значение в следующем смысле:

Если набор пунктов $ f $ подразумевает не тавтологический пункт $ C $, то всегда можно получить единый пункт $ C '$, который подчиняется $ C $ (то есть $ C' subteq C $).

Источник:
Кристиан Г. Фермуллер, Полнота подписанной резолюции, 2002

Обратите внимание, что исходный результат упоминается:
RCT Lee. Теорема полноты и компьютерная программа для теоремы, полученных из данных аксиомов. Кандидат наук. Тезис, Калифорнийский университет, Беркли, 1967.