Контрольная работа по "Математическая логика и теория алгоритмов"

$x$y$z$u$v((ØP(f(x, y), z) & ØP(f(x, z), y) & ØP(f(y, z), x)) Ú P(g(u), v)))

Получена  предваренная форма. Получим из нее  скорлемовскую форму:

6. Поставим каждой $-квантифицированной переменной функциональную форму от предшествующих ей в префиксе "-квантифицированных переменных:

x – a;

y –  b;

z –  c;

u –  d;

v –  f.

7. Подставим в формулу функциональные формы и удалим $-квантификацию:

 ((ØP(f(a, b), c) & ØP(f(a, c), b) & ØP(f(b, c), a)) Ú P(g(d), f)))

Получили  Сколемовскую форму.

8. Приведем к КНФ:

   ((ØP(f(a, b), c) Ú P(g(d), f)) & (ØP(f(a, c), b) Ú P(g(d), f)) & (ØP(f(b, c), a) Ú P(g(d), f)))

   Имеем множество дизъюнктов (клаузальную форму):

   {ØP(f(a, b), c) Ú P(g(d), f), ØP(f(a, c), b) Ú P(g(d), f), ØP(f(b, c), a) Ú P(g(d), f)}. 

6.1  Определить наиболее общий унификатор и соответствующий ему общий пример для следующего множества термов или показать, что множество неунифицируемо.

е)  {g(f(b), f(x), a), g(y, v, b)}

Решение:

      Построим  унификатор в соответствии с алгоритмом:

1. k:=0, s₀:=e (пустая подстановка).

   Имеем s₀○L_i={g(f(b), f(x), a), g(y, v, b)}. Элементы множества различны, поэтому переходим к составлению множества рассогласования.

2. B₀={f(b), y}, отсюда s₁:= {(y, f(b))}○e = {(y, f(b))}.

s₁○L_i={g(f(b), f(x), a), g(f(b), v, b)}. Элементы множества различны, поэтому переходим к составлению множества рассогласования.

3. B₁={f(x), v}, отсюда s₂:= {(f(x), v)}○ s₁ = {( y, f(b)), (f(x), v)}.

s₂○L_i={g(f(b), f(x), a), g(f(b), f(x), b)}. Элементы множества различны, поэтому переходим к составлению множества рассогласования.

B₂={a,  b}. Множество неунифицируемо. 

6.2 Записать следующее рассуждение на языке логики предикатов и доказать его справедливость, используя метод резолюций.

в) Посылки: Арт - мальчик, у которого нет автомобиля. Джейн любит только мальчиков, имеющих автомобили.

Заключение: Джейн не любит Арта.

Решение:

      Введем  необходимые формальные обозначения: P(x) – «x – мальчик»; Q(x) – «x имеет автомобиль»; L(x, y) – «x любит y»; a – «Арт»; d – «Джейн». Тогда данное рассуждение запишется следующим образом:

{P(a) & ØQ(a), "x(P(x) & L(d, x) ® Q(x))} ╞ ØL(d, a).

Переносим заключение в левую часть с  отрицанием:

{P(a) & ØQ(a), "x(P(x) & L(d, x) ® Q(x)), ØØL(d, a)}.

      Преобразование  формул в клаузальную форму:

1. P(a) & ØQ(a). Получим множество дизъюнктов: {P(a), ┐Q(a)}.
2. "x(P(x) & L(d, x) ® Q(x)). Формула в предваренной форме. Преобразуя в КНФ, получим:  "x(ØP(x) Ú ØL(d, x) Ú Q(x))
3. L(d, a).

Получили  множество дизъюнктов:

1. P(a);
2. ØQ(a);
3. ØP(x) Ú ØL(d, x) Ú Q(x);
4. L(d, a).

Применяя  правило резолюции и унификацию, получим следующий вывод (в скобках  указаны номера родительских дизъюнктов и унификатор):

5. ØL(d, a) Ú Q(a) (1, 3   s₁= {(x, a)});
6. ØL(d, a) (2, 5);
7. F (4, 6).

Справедливость  утверждения доказана. 

   д)  Посылки: Ни один республиканец или демократ не является социалистом. Норман Томас – социалист.

   Заключение: Норман Томас – не республиканец.

Решение:

      Введем  необходимые формальные обозначения: P(x) – «x – респобликанец»; Q(x) – «x – демократ»; R(x) – «x – социалист»; a – «Норман Томас». Тогда данное рассуждение запишется следующим образом:

{┐$x((P(x) Ú Q(x)) & R(x)), R(a)} ╞ ┐P(a).

Переносим заключение в левую часть с  отрицанием:

{┐$x((P(x) Ú Q(x)) & R(x)), R(a), ┐┐P(a)}.

      Преобразование  формул в клаузальную форму:

1. ┐$x((P(x) Ú Q(x)) & R(x)) = "x┐((P(x) Ú Q(x)) & R(x)). Формула в предваренной форме. Преобразуя в КНФ, получим:  "x((┐P(x) Ú ┐R(x)) &(┐Q(x) Ú ┐R(x))) Получим множество дизъюнктов: {┐P(x) Ú ┐R(x), ┐Q(x) Ú ┐R(x)}.
2. R(a). Формула уже в клаузальной форме.
3. ┐┐P(a) = P(a).

Получили  множество дизъюнктов:

1. ┐P(x) Ú ┐R(x);
2. ┐Q(x) Ú ┐R(x);
3. R(a);
4. P(a).

 Применяя правило резолюции и унификацию, получим следующий вывод (в скобках указаны номера родительских дизъюнктов и унификатор):

5. ┐P(a) (1, 3   s₁= {(x, a)});
6. Fkj . (4, 5).

Справедливость  утверждения доказана.