Предикатов.

Не существует четких правил и рекомендаций, как представить в виде формулы логики предикатов то или иное умозаключение. Все это делается интуитивно. А интуиция находится в пропорциональной зависимости от мастерства в доказательстве теорем методом резолюций. Поэтому только через практику и навыки можно приобрести необходимую интуицию для моделирования умозаключений. В какой-то мере стартовую интуицию можно приобрести, ознакомившись с приведенными ниже примерами, рассмотренными в различных работах [4,6,7,11,12]. В первых двух примерах приводятся достаточно подробные объяснения, в остальных – только по мере надобности.

Пример 1. Некоторые пациенты любят своих докторов. Ни один пациент не любит знахаря. Следовательно, никакой доктор не является знахарем.

Введем следующие обозначения для предикатных символов: - пациент, - доктор, - знахарь, - любит.

Тогда перечисленные ниже предикаты будут обозначать:

— есть пациент;

— есть доктор;

— есть знахарь;

— любит .

Факты и заключение, приведенные в рассуждении, могут быть представлены следующими формулами:

Факт 1

Факт 2

Заключение

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

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

из

Здесь действует правило 2а из 2.3.6.1 , правило исключения кван- тора существования и правило исключения связки импликации.

из

из

 

Выполняя унификации и склейки, получим:

резольвента (2) и (4).

резольвента (1) и (3).

резольвента (5) и (7).

резольвента (6) и (8).

Теорема доказана.

Пример 2. Все люди – животные. Следовательно, голова человека является головой животного.

Пусть есть следующие предикаты:

— есть человек;

— есть животное;

— является головой .

Необходимо доказать теорему:

 

 

Преобразование числителя (теоремы-посылки) дает дизъюнкт:

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

.

Тогда

Применяя метод резолюций, получим:

из (1) и (2).

из (4) и (5).

из (3) и (6).

Теорема доказана.

Пример 3. Посылки: таможенные чиновники обыскивают каждого, кто въезжает в страну, кроме высокопоставленных лиц. Некоторые лица, способствующие провозу наркотиков, въезжают в страну и обыскиваются исключительно людьми, также способствующими провозу наркотиков. Никто из высокопоставленных лиц не способствовал провозу наркотиков.

Заключение: некоторые из таможенников способствовали провозу наркотиков.

Введем следующие обозначения для предикатов:

въезжал в страну;

был высокопоставленным лицом;

обыскивал ;

был таможенником;

способствовал провозу наркотиков.

Посылки представляются следующими формулами:

а заключение теоремы – формулой:

Преобразуя посылки в дизъюнкты, получим:

Отрицание заключения:

Доказательство методом резолюций выглядит следующим образом:

из (3) и (6).

из (2) и (4).

из (8) и (9).

из (1) и (4).

из (8) и (11).

из (12) и (5).

из (7) и (13).

из (10) и (14).

Заключение доказано.

Пример 4. Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один из преподавателей не является невеждой.

Обозначим:

— есть студент;

— есть преподаватель;

— есть невежда;

— любит .

На языке логики предикатов после приведения к стандартному виду это запишется так:

Преобразование двух теорем-посылок числителя дает следующие дизъюнкты:

.

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

что дает дизъюнкты:

Путем унификации и склеек получим:

из (2) и (4).

из (1) и (3).

из (5) и (7).

из (6) и (8).

Теорема доказана.