Матлогика, теория автоматов

Question

Доказать теорему, используя метод резолюции:
А1. Никто, кроме птиц, не имет перьев.
А2. Ни одна птица не является рыбой.
Т: Ни одна рыба не имет перьев.

Прошу помочь, ибо не успеваю и немного не могу в матлогику.

Answer 1

Если не ошибаюсь, то будет так
1. Вводим три элементарных высказывания
Х1 - объект является птицей
Х2 - объект является рыбой
Х3 - у объекта есть перья.

2. Записываем аксиомы и теорему в этих термах

А1 = ^X1-^X3
A2 = X1-^X2
T = X2-^X3

3. Переводим выражения в КНФ
А1 = X1 v ^X3
A2 = ^X1 v ^X2
T = ^X2 v ^X3

4. Находим отрицание теоремы ^T = X2 & X3

5. Получаем начальный набор дизъюнктов

 (X1 v ^X3) , (^X1 v ^X2) , X2, X3

6. Применяем правило резолюции к 1 и 2 дизъюнкту, получаем
 (X1 v ^X3) , (^X1 v ^X2) , X2, X3, ^X2, ^X3

7. Применяем правило резолюции к 3 и 5 дизъюнкту, получаем
 (X1 v ^X3) , (^X1 v ^X2) , X2, X3, ^X2, ^X3, 0 (пустой дизъюнкт)
Из множества аксиом и отрицания теоремы выведен пустой дизъюнкт, значит исходная теорема верна, т. е. " рыба не имет перьев".