Унификация и склейка

[damir_777]

Предположим, что дан следующий дизъюнкт:
$p(x,f(y,z)) \vee p(x,f(g(x),z)) \vee p(x,f(a,x))$
Рассогласование следующее: $y, g(x), a$
У меня вот такой вопрос: В примерах алгоритма унификации и склейки дизъюнкта всегда приводятся примеры унификации только пары дизъюнктов. Здесь же даны сразу три дизъюнкта. Как поступать в таких случаях? Т.е нужно также рассматривать комбинации дизъюнктов, т.е сначала попытаться найти унификатор для 1 и 2 дизъюнкта, потом для 1 и 3 ,а потом для 2 и 3? И если их рассматривать парами , то получается при первом же найденном унификаторе уже можно не рассматривать остальные комбинации, а сразу применить склейку к дизъюнкту?
Второй вопрос про склейку. Прежде чем применять правило резолюции одного дизъюнкта с другим в каждом дизъюнкте если имеется возможность нужно провести склейку.
Предположим дан следующий дизъюнкт (Термы писать не буду , только литеры):
$P(...) \vee P(...) \vee P(...) \vee Q(...) \vee Q(...)$
Предположим что найден унификатор по литерам $P$. Нужно ли также искать унификатор по $Q$? Или если найден унификатор по какой-нибудь литере то можно сразу производить склейку и имеет ли значение какой унификатор применять: по $P$ или по $Q$
Т.е у меня непонимание по этой теме когда рассматривается не пара дизъюнктов , а большее их количество

[damir_777]

Или к примеру если дан дизъюнкт $L_1 \vee L_2 \vee L_3 \vee ... \vee L_n$, где все L- однополярные литеры имеющие одну и ту же литеру, то по какому правилу проводить склейку, т.е нужно ли склеивать их все где есть возможность или достаточно остановиться найдя какой нибудь общий унификатор для двух, а потом применить склейку

[Toucan]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
по следующим причинам:

- неправильно набраны формулы (краткие инструкции: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы).

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Lia]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»

[mihailm]

(Оффтоп)

Мало чего понял, но вопрос возник. А конструкция с $\wedge$ называется конъюнкт?

[damir_777]

Нет, вообще речь идет о методе резолюции. Дано множество дизъюнктов Прежде чем применять правило резолюции к паре дизъюнктов, нужно если есть возможность провести склейку предикатов в каждом дизъюнкте. Выше я и привел примеры предикатов, вот меня и интересует это правило, а то в интернете да и в Гугле что то наткнулся на примеры склейки всего двух предикатов, а если их больше?

-- 06.04.2016, 21:53 --

mihailm в сообщении #1112805 писал(а):

(Оффтоп)

Мало чего понял, но вопрос возник. А конструкция с $\wedge$ называется конъюнкт?

КНФ-конъюнктивная нормальная форма

-- 06.04.2016, 22:36 --

Вот более подробный приведу пример
Предположим даны дизъюнкты:
$C_1=P(x) \vee P(f(y)) \vee Q(x)$
$C_2= \neg P(f(g(a))) \vee Q(b) $
Т.к как есть две контрарные литеры , мы можешь применить правило резолюции, но также в дизъюнкте $C_1$ имеются две одинаковые литеры P. Поэтому их можно склеить.
А теперь представит что дизъюнкт $C_1$ имеет следующую форму (термы в скобках писать не буду)
$C_1=P(...) \vee P(...) \vee P(...) \vee P(...) \vee Q(...) \vee Q(...) \vee Q(...)$
Т.е вообще говоря имеется несколько одинаковых литер, больше двух. Тогда вот здесь какое правило склейки, ну т.е то что я писал выше