Лок-резолюция

[damir_777]

Здравствуйте
Есть следующий пример из книги Чень Ли Автоматическое доказательство теорем (стр. 124-125)
Дан набор дизъюнктов:
1.$ P_5(y,a) \vee P_1(f(y),y) $
2.$ P_6(y,a) \vee P_2(y,f(y)) $
3.$ \neg P_8(x,y) \vee P_3(f(y),y) $
4.$ \neg P_9(x,y) \vee P_4(y,f(y)) $
5.$ \neg P_1_0(x,y) \vee \neg P_7(y,a) $
Лок-вывод:
6.$ P_5(a,a) \vee \neg P_1_0(x, f(a)) $ лок-резольвента 1 и 5
7.$ \neg P_8(x,a) \vee \neg P_1_0(y,f(a)) $ лок-резольвента 3 и 5
8.$ \neg P_1_0(x,f(a)) \vee \neg P_1_0(y,f(a)) $ лок-резольвента 6 и 7
9.$ P_6(a,a) $ лок-резольвента 8 и 2
10.$ \neg P_9(x,a) $ лок-резольвента 8 и 4
11.$ \square $ лок-резольвента 9 и 10
Я не пойму как получился вывод 6.$ P_5(a,a) \vee \neg P_1_0(x, f(a)) $ лок-резольвента 1 и 5
По правилу лок-резолюции сравниваются две литеры, имеющие наименьшие индексы, в данном случае $ P_1(f(y),y) $ из набора (1) и \neg $ \neg P_7(y,a) $ из набора (5). Эти литеры имеют наименьшие индексы и контрарны. Теперь необходимо их унифицировать. Первое рассогласование это f(y) из литеры $ P_1 $ и y из $ \neg P_7$. Получается подстановка f(y)/y, но переменная y содержится в терме f(y), и значит по определению алгоритма унификации эти литеры не унифицруемы, однако в данном примере как то получена лок-резольвента. И вообще я получил, что этот набор дизъюнктов выполним, а в примере получен пустой дизъюнкт. Объясните, это опечатка в книге или я что то неправильно делаю

Второй вопрос хотел задать именно по алгоритму лок-резолюции. Нужно ли в нем реализовывать алгоритм поглощения, т.е проверять, является ли определенный дизъюнкт поддизъюнктом другого дизъюнкта. Например, в методе насыщения уровня, такая проверка нужна, чтобы не получать повторяющихся дизъюнктов. Или может сам метод лок-резолюции обеспечивает то, что появлющиеся лок-резольвенты не будут поглощаться никакими вышележащими дизъюнктами.
К примеру, даны два дизъюнкта: (Чень Ли Автоматическое доказательство теорем (стр. 99-100))
C=$ \neg P(x) \vee Q(f(x),a) $
D=$ \neg P(h(y)) \vee Q(f(h(y)),a) \vee P(z) $
Необходимо проверить, является ли C поддизъюнктом D
По алгоритму поглощения для D находится подстановка $ \sigma={b/y, c/z} $, далее
$ \neg D\sigma=P(h(b)) \wedge \neg Q(f(h(b)),a) \wedge P(c) $
Теперь загоняем $ \neg D\sigma $ в список W, а С в список U
$ W={P(h(b)), \neg Q(f(h(b)),a), P(c)}$
$ U={\neg P(x) \vee Q(f(x),a)}$
Теперь с помощью обычного резолютивного вывода находим резольвенты, резольвируя каждый дизъюнкт из W c U.
Получается $ U={Q(f(h(b)),a), \neg P(h(b)), Q(f(c), a)} $. И снова резольвируя W c только что полученной U, будет найден пустой дизъюнкт, а это значит что C поглощается D.
Теперь, т.к все резольвенты находятся с помощью лок-резолюции, то я попытался применить ее к алгоритму поглощения.
Однако, если я буду делать то же самое, но вместо обычного вывода, использовать лок-резолюцию, то у меня получится при первом выводе
$ U={Q(f(h(b)),a), Q(f(c), a)} $, т.е здесь отсутствует второй дизъюнкт. И в дальнейшем опять применяя вывод к новой U, я уже не получу пустого дизъюнкта, и это будет говорить о том, что C не будет поддизъюнктом D.
Конечно, если алгоритм поглощения можно не использовать, то вопрос отпадает сам собой.

[iifat]

Стоило б тщательнее как-то перепечатывать — если, конечно, вам нужен ответ. В первом примере присутствует один предикат, числа нумеруют вхождения.
А насчёт «как» — ну, пишем один прод другим, решаем, какой исключить (вторые из обеих высказываний), сопоставляем переменные ($f(y_1)=y_5, y_1=a$, индексы у переменных тут — номера уравнений), так чтобы исключаемые совпали, подставляем в оставшиеся, кои совокупляем в единое высказывание — вот и всё.

[damir_777]

да вообще то тщательнее то некуда), я перепечатал все как в книге, но вот у вас появляются индексы у переменных. С этим я че то не сталкивался , да и в книге про это нету. Т.е нужно еще переменные нумеровать?

[iifat]

Ну, вообще-то, $\mathstrut_5P(x,y)$ и $P_5(x,y)$ — две большие разницы.
Нумерацию переменных поставил я, чтоб стало понятнее.
Вам нужно найти две формулы $A\vee B, \neg A\vee C$ и вывести из них третью: $B\vee C$. Поскольку речь идёт о предикатах с параметрами, предварительно нужно привести оные к одному виду. В книге этот этап оставляют на ваше усмотрение и потому никак не обозначают.

[damir_777]

теперь кажется понял
У меня не получился вывод, потому что получилась подстановка f(y)/y, и переменная содержится в терме. Но если я каждой переменной задам различные индексы, например, по номеру дизъюнкта , то получится $ f(y_1)/y_5$ и уже переменная не содержится в терме и можно найти подстановку.
В общем случае мне, я так понял нужно переписать все так:
1.$ _5P(y_1,a) \vee _1P(f(y_1),y_1) $
2.$ _6P(y_2,a) \vee _2P(y_2,f(y_2)) $
3.$ \neg _8P(x_3,y_3) \vee _3P(f(y_3),y_3) $
4.$ \neg _9P(x_4,y_4) \vee _4P(y_4,f(y_4)) $
5.$ \neg _1_0P(x_5,y_5) \vee \neg _7P(y_5,a) $
А в лок-выводе, например, 6 я должен тоже присвоить новые индексы, т.е получается новая строка-новые индексы
6.$ _5P(a,a) \vee \neg _1_0P(x_6, f(a)) $ лок-резольвента 1 и 5

[iifat]

Для пущей точности: все переменные мыслятся связанными. То бишь, первая, скажем, строчка на самом деле записывается так: $\forall y (P(y,a)\vee P(f(y),y))$. Циферки слева внизу нумеруют вхождения одного и того же предиката и используются для выбора, какой предикат исключать, какой оставить — в вашей книжке про это написано, не стал внимательно читать. $y$, будучи связанной переменной, может называться как угодно, в том числе одинаково в разных строках. Пока не набьёте руку, действительно стоит их обозначать по-разному.

[damir_777]

еще хотел задать небольшой вопрос по расстановке индексов.
Есть ли какая нибудь разница если я например буду последовательно расставлять индексы от 1 и до n либо в обратном порядке, т.е будет ли меняться количество шагов до вывода пустого дизъюнкта (если набор дизъюнктов будет невыполним) ю К примеру если я поставлю индексы в прямом порядке то допустим будет выполнено 6 шагов, в обратном например 7 или независимо от этого всегда кол-во шагов будет одинаковым?
а второй вопрос такой
По теореме о полноте лок резолюция всегда выводит пустой дизъюнкт, т.е получается что это гарантия того что как бы я не расставил индексы будет получен пустой дизъюнкт?

[iifat]

Ну, я почитал минимально и не до конца понял. От расстановки индексов, разумеется, зависит ход вывода, в том числе, по идее, число шагов.

damir_777 в сообщении #1126704 писал(а):

По теореме о полноте

Опять же, до теоремы не дочитал, но коли уж таковая есть, доказана и условия её выполняются, то и выводы должны быть верны Я ещё почитаю, может, добавлю.