В соответствии с вариантом. Бесплатный доступ к контрольной работе

Зарегистрируйся в 2 клика в Кампус и получи неограниченный доступ к материалам с подпиской Кампус+ 🔥

Условие

В соответствии с вариантом (табл. П4 приложения): 1) преобразовать формулу ЛП к ПНФ; 2) полученную в п.1 формулу привести к ССФ; 3) по матрице ССФ, полученной в п.2, сформировать множество дизъюнктов К и выполнить их унификацию. Приложения Приложение 4. Варианты по теме «Логика предикатов» Таблица П4 Вариант Формула 1 2 3 ∀xAx→∃zBz→∀zBx→Cz→Cz

Нужно полное решение этой работы?

Решение

Потяни, чтобы посмотреть

1. Преобразование формулы ЛП к ПНФ
1)исключим в формуле всюду логические связки → в соответствии с законами ЛВ импликации:
∀xAx→∃zBz→∀zBx→Cz→Cz =
∀xAx ∃zBz ∀zBx Cz Cz;
2) продвигаем знаки отрицания до элементарной формулы, используя закон отрицания кванторов ЛП и закон де Моргана ЛВ:
∀xAx ∃zBz ∀zBx Cz Cz =
∀xAx&∃zBz ∀zBx&Cz Cz =
∀xAx&∀zBz ∀zBx&Cz Cz =
∀xAx&∀zBz ∀zBx Cz;
3)заменяем связанные переменные. Для этого выполняем следующие действия:
• находим в формуле самое левое связанное вхождение переменной и, в случае необходимости, заменяем ее . В нашей формуле первый слева квантор всеобщности связывает переменную х, которая далее входит в предикат В(х) свободно, поэтому требуется замена переменной х в крайнем левом вхождении; приведенное выражение изменится с помощью операции подстановки: xx1∀xAx∀x1Ax1 ;
• следующими идут два квантора всеобщности ∀z, поэтому переменную z, связанную вторым квантором всеобщности, заменяем с помощью операции подстановки: zz1∀zBz∀z1Bz1 ;
4)выносим кванторы в префикс, не нарушая их последовательности:
∀x1Ax1&∀z1Bz1 ∀zBx Cz =
∀x1∀z1∀zAx1&Bz1 Bx Cz;
5) производим преобразование матрицы к КНФ:
∀x1∀z1∀zAx1&Bz1 Bx Cz =
∀x1∀z1∀zAx1 Bx Cz&Bz1 Bx Cz .
Таким образом, полученная формула представлена в виде ПНФ: она имеет две зоны – префикс в виде ∀x1∀z1∀z и бескванторную матрицу в формате КНФ – Ax1 Bx Cz&Bz1 Bx Cz .
2

50% задачи недоступно для прочтения

Переходи в Кампус, регистрируйся и получай полное решение

Получить задачу