Объединение логического разрешения первого порядка
Вопрос
Предполагая, что я показал часть базы знаний в формате клаузала:
[1] p1(banana).
[2] not p1(X) or p2(Y).
[3] p1(X) or not p3(F).
... и больше правил.
Большинство книг сделают что -то вроде этого:
[1,2] {X=banana} p2(Y).
и больше шагов.
Первый вопрос: верно ли делать что -то вроде следующего:
[2,3] {X=X} p2(Y) or not p3(F).
а затем продолжить с разрешением.
Второй вопрос: что, если бы в каждом пункте использовались разные переменные, я мог бы сделать то же самое, что и выше, например, у нас было:
[2] not p1(X1) or p2(Y1).
[3] p1(X2) or not p3(F2).
[2,3] {X1=X2} p2(Y) or not p3(F2).
заранее спасибо
Решение
Предполагая, что $ x $ здесь является переменной, а не атомным предложением, то сначала вы должны указать, что такое количественная оценка для 2 и 3. Я предполагаю, что это должно быть
$ forall x, y neg p1 (x) vee p2 (y) $, и аналогично 3. В этом случае, что можно сделать, так это заменить $ x $ и $ y $ на каждое атомное предложение, доступное, в порядок получить пропозициональную базу знаний и работать над этим.
То, что вы предлагаете делать с 2,3, звучит только при универсальной количественной оценке, но если у вас есть только универсальная количественная оценка, это действительно полезно.
Для вашего второго вопроса: имя переменной ничего не значит, поэтому ваша замена также звучит. Действительно, претензия $ forall y, p (y) $ эквивалентна $ forall z, p (z) $. Сначала вы можете изменить имена, если это делает вас счастливым :)
Я замечаю, что обычно, в доказательствах под руководством разрешения, более полезно разрешить конкретное выражение с количественным правилом. Например, разрешение $ p (a) $ с $ forall xp (x) to q (x) $, чтобы получить $ q (a) $. Это более вероятно (эвристически), чтобы заставить вас подтвердить претензию.