Метод резолюций и его применение в алгебре высказываний и алгебре предикатов

Применение стратегии  к прежнему множеству дизъюнктов дает следующее:

S0: (1) X Y, 

  (2) ,  

          (3) X Z, 

  (4) Z, 

  (5) , 

S1: (6) Z        из (2) и (3), 

(7) Y Z         из (1) и (4), 

          (8) Z               из (3) и (4),

          (9) X               из (3) и (5),

          (10)            из (4) и (5),

          (11)             из (5) и (6),

          (12) Y             из (5) и (7),

          (13) □              из (5) и (8).

Рассмотренные стратегии  являются полными в том смысле, что если множество дизъюнктов S невыполнимо, то из S пользуясь стратегией можно вывести пустой дизъюнкт. Для первых двух стратегий это достаточно очевидно. Полнота стратегии вычеркивания следует из того, что если D и C–дизъюнкты из S и D – расширение C, то множество S невыполнимо в том и только в том случае, когда невыполнимо множество S\{D}.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Примеры использования  метода резолюций.

Рассмотрим примеры, чтобы  продемонстрировать, как можно эффективно использовать метод резолюций для доказательства теорем.

Пример 1. Предположим, что  курс акций падает, если предварительные  процентные ставки растут. Предположим  также, что большинство людей  несчастны, когда курс акций падает. Положим, что предварительные процентные ставки растут. Из этого можно заключить, что большинство людей несчастны.

Чтобы установить это  заключение, обозначим утверждения  следующим образом:

Р: предварительные процентные ставки растут;

S: курс акций падает;

U: большинство людей несчастны.

Тогда имеем четыре утверждения:

(1') P S,

(2') S U,

(3') P,

(4') U.

Чтобы показать, что (4') следует из (1'), (2') и (3') мы сперва преобразуем все утверждения в стандартную форму. Таким образом, имеем

(1) ,

(2) ,

(3) P,

(4) U.

Докажем путём опровержения, что U – логическое следствие из (1), (2) и (3). Отрицаем (4) и получаем следующее доказательство:

(1) ,

(2) ,

(3) P,

(4)       отрицание заключения,

(5)  S      резольвента (3) и (1),

(6)  U     резольвента (5) и (2),

(7)  □      резольвента (6) и (4).

Пример 2.Допустим, что если конгресс отказывается принять новые законы, то забастовка не будет окончена, если только она не длится более года и президент фирмы не уходит в отставку. Закончится ли забастовка, если конгресс отказывается действовать, и забастовка только что началась?

Преобразуем утверждения  в формулы:

Р: конгресс отказывается действовать;

Q: забастовка оканчивается;

R: президент фирмы уходит в отставку;

S: забастовка длится более года.

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

         - если конгресс отказывается принять новые законы, то забастовка не будет окончена, если она не длится более года и президент фирмы не уходит в отставку.

- конгресс отказывается действовать.

- забастовка только что началась.

Итак, имеем три формулы , и , хотим доказать, что - логическое следствие . Отрицаем и приводим в стандартную форму. Это приводит к следующему множеству дизъюнктов:

,

(3) P           из ,

(4)          из ,

(5)  Q         отрицание заключения,

Использую резолюцию, мы получим следующее доказательство:

(6)      резольвента (3) и (2),

(7)   S         резольвента (6) и (5),

(8)   □         резольвента (7) и (4).

Пример 3. Рассмотрим следующее  множество формул:

Наша задача, доказать, что G является логическим следствием и . Преобразуем , и в стандартную форму и получим следующие пять дизъюнктов:

,

,

 из  .

Это множество дизъюнктов невыполнимо. Это можно доказать с помощью методе резолюций следующим образом:

(6)   резольвента (3) и (2),

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

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

Таким образом, G - логическое следствие и .

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

P(x): x – пациент,

D(x): x – доктор,

Q(x): x – знахарь,

L(x, y): x любит y.

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

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

(3) из ,

.

Используя метод резолюций, получим следующее доказательство:

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

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

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

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

Метод резолюций совершенно естествен. Попытаемся перевести предыдущее доказательство на русский язык:

1. Из можем предположить, что существует пациент , который любит каждого доктора (дизъюнкты (1) и (2)).
2. Предположим, что заключение неверно, то есть предположим, что - одновременно и доктор и знахарь(дизъюнкты (4) и (5)).
3. Так как пациент любит каждого доктора, то любит (дизъюнкт (6)).
4. Так как - пациент, то не любит никакого знахаря (дизъюнкт (7)).
5. Однако -знахарь, значит не любит (дизъюнкт (8)).
6. Это невозможно из-за (с). Таким образом, мы закончили доказательство.

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

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

Пусть Е(х) означает «х въезжал  в страну», V(x) означает «х был высокопоставленным лицом», S(x,y) означает «у обыскивал х», С(х) означает «х был таможенником», Р(х) означает «х способствовал провозу наркотиков».

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

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

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

(1)

(2)

(3) Р(а),

(4) Е(а),

(5) ,

(6)

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

(7)

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

(8)                        из (3) и (6),

(9)         из (2) и (4),

(10)                 из (8) и (9),

(11)    из (1) и (4),

(12)              из (8) и (11),

(13)                 из (12) и (5),

(14)                из (13) и (7),

(15) □                          из (10) и (14).

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

Пример 6. Посылка такая: каждый, кто хранит деньги, получает проценты. Заключение: если не существует процентов, то никто не хранит денег. Пусть S(x, y), M(x), I(x) и E(x, y) означают «х  хранит деньги у», «х есть деньги», «х есть проценты» и «х получает у» соответственно. Тогда посылка записывается в виде:

 

а заключение – в виде

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

(1) 

(2) 

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

(3) ,

(4) ,

(5) .

Дальнейшее доказательство на самом деле очень просто:

(6)      из (3) и (1),

(7)                  из (6) и (4),

(8)  □                       из (7) и (5).

Таким образом, заключение доказано.

Пример 7. Посылка: студенты суть граждане. Заключение: голоса студентов  суть голоса граждан.

Пусть S(x), C(x) и V(x, y) означают «х – студент», «х - гражданин» и «х есть голос у» соответственно. Тогда посылка и заключение запишутся следующим образом:

                                                          (посылка),

              (заключение).

Стандартная форма посылки  есть:

(1)

Так как

=   =

=

Имеем три дизъюнкта  для отрицания заключения:

(2) ,

(3) ,

(4) 

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

(5)           из (1) и (2),

(6)       из (5) и (4),

(7) □               из (6) и (3).

Снова, хотя указанное  доказательство строится вполне механически, оно в действительности очень  естественно. На самом деле мы можем  перевести это доказательство на русский язык следующим образом. Предположим, что  - студент, есть голос и не является голосом какого-либо гражданина. Так как - студент, то должен быть гражданином. Кроме того не должен быть голосом , так как - гражданин. Это невозможно. Таким образом, мы закончим доказательство.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Заключение.

В нашей курсовой работе мы рассмотрели историю появления, назначение и применение метода резолюций. Изучив литературу по данной  теме, разобрали основные стратегии, применяемые к решениям задач с использованием метода резолюций в логике высказываний и  логике предикатов. И показали применение принципа резолюций на практике, решив несколько задач. Считаем, что данная курсовая работа будет полезна при изучении основ логического программирования, решающего большинства задач искусственного интеллекта, в основе которого и лежит метод резолюции для логики предикатов первого порядка.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Список используемой литературы:

1. Чень Ч. ,Ли Р. - Математическая логика и автоматическое доказательство теорем, Наука, 1983 г.
2. Тей А.,Грибомон П.,Луи Ж. - Логический подход к искусственному интеллекту. От классической логики к логическому программированию (Пермяков П.П., Гаврилов Г.П.), Мир, 1990 г.
3. Игошин В.И. - Математическая логика и теория алгоритмов : учеб. пособие для студ. высш. учеб. заведений / В. И. Игошин. — 2-е изд., стер. — М. : Издательский центр «Академия», 2008.
4. Робинсон - Машинно-ориентированная логика, основанная на принципе резолюций//Кибернетический сборник, 1970, вып.7.
5. http://pgap.chat.ru/zap/zap13.htm#0
6. http://www.intuit.ru/department/pl/plprolog/
7. http://it.kgsu.ru/Prolog/