русс | укр

Языки программирования

ПаскальСиАссемблерJavaMatlabPhpHtmlJavaScriptCSSC#DelphiТурбо Пролог

Компьютерные сетиСистемное программное обеспечениеИнформационные технологииПрограммирование

Все о программировании


Linux Unix Алгоритмические языки Аналоговые и гибридные вычислительные устройства Архитектура микроконтроллеров Введение в разработку распределенных информационных систем Введение в численные методы Дискретная математика Информационное обслуживание пользователей Информация и моделирование в управлении производством Компьютерная графика Математическое и компьютерное моделирование Моделирование Нейрокомпьютеры Проектирование программ диагностики компьютерных систем и сетей Проектирование системных программ Системы счисления Теория статистики Теория оптимизации Уроки AutoCAD 3D Уроки базы данных Access Уроки Orcad Цифровые автоматы Шпаргалки по компьютеру Шпаргалки по программированию Экспертные системы Элементы теории информации

Доказательство методом резолюции

Применяется всего одно правило вывода, что позволяет не запоминать многочисленных правил вывода и тавтологии. Это- правило резолюции, которое приведено  в таблице 2.1 вместе с уже известными правилами.

 

Таблица 2.1

Резолюция

Цепное правило

Модус поненс

Из Х А

Из ~Х-->А

А

И Y ~А

И А-->Y

А-->Y

Получаем Х Y

Получаем ~Х-->Y

Y

 

Оно позволяет соединить две формулы, удалив из одной атом А а из другой ~А. Из приведенной выше таблицы видно, что правило резолюции можно рассматривать как аналог цепного правила в применении к формулам, находящимся в конъюнктивной нормальной форме В данном случае цепное правило записано в форме, эквивалентной приведенной ранее, но более удобной для сопоставления с правилом резолюции. Правило модус поненс можно считать частным случаем правила резолюции для случая ложного X.

Правило резолюции применяем следующим образом.

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

Приводим все посылки и отрицание заключения, принятого в качестве дополнительной посылки, к конъюнктивной нормальной форме.

а) Устраняем символы <-->и--> с помощью эквивалентностей

       (А<-->В) = (А-->В)  C)(В-->А);

A-->В = ~А В

      б) Продвигаем отрицания внутрь с помощью закона де Моргана.

в) Применяем дистрибутивность

А (B C)=(A B)(A C).

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

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

Теперь каждая посылка превратилась в конъюнкцию дизъюнктов, быть может, одночленную. Выписываем каждый дизъюнкт с новой строки; все дизъюнкты истинны, так как конъюнкция истинна по предположению.

Каждый дизъюнкт- это дизъюнкция (возможно, одночленная), состоящая из предложений и отрицаний предложений. Именно к ним применим метод резолюций. Берем любые два дизъюнкта, содержащие один и тот же атом, но с противоположными знаками, например

Х  Y  Z  ~P,   X  P  W.

Здесь Р - как раз тот атом, о котором шла речь. Применяем правило резолюции с атомом Р в роли А из этого правила, т.е. "отрезаем" Р от двух данных дизъюнктов:

YZ)(YW)=XYZW.

Это правило легко применять, так как оно сводится к простому удалению членов дизъюнктов.

Из ХA,~AY выводим ХY.

Из A, ~AY выводим Y.

Продолжаем этот процесс, пока не получится Р и ~Р для некоторого атома Р. Применяя резолюцию и к ним, получим пустой дизъюнкт, выражающий противоречие, что завершает доказательство от противного.

Из Р, ~Р выводим ложь.

Пустой дизъюнкт обычно записывается в виде квадрата ?.

В качестве примера рассмотрим доказательство соотношения:

PQ, P-->R, Q-->S|-R S

  • Приводим посылки к нормальной форме и выписываем их на отдельных строках.

P Q,                                                                      (2.12)

~ P R,                                                                   (2.13)

~Q S                                                                      (2.14)

  • Записываем отрицание заключения и приводим его к нормальной форме.

~(R S)= ~R~S                                                             

~R                                                                                  (2.15)

~S                                                                                  (2.16)

  • Выводим пустой дизъюнкт с помощью резолюции.

 

~Р из (2.15) и (2.13)                                                    (2.17)

Q из (2.17) и (2.12)                                                             (2.18)

~Q из (2.16) и (2.14)                                                            (2.19)

? из (2.18) и (2.19)                                                               (2.20)

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

  1. Не приходится применять эквивалентности для того, чтобы переставлять члены дизъюнкции Р Q для получения Q P и т.д. Это происходит отчасти потому, что все приводится к нормальной форме с самого начала, а отчасти потому, что для правила резолюции неважно положение отрезаемого атома в дизъюнкте.
  2. Нужно помнить всего одно правило.

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

Просмотров:

Вернуться в оглавление:Экспертные системы



Карта сайта Карта сайта укр


Уроки php mysql Программирование

Онлайн система счисления Калькулятор онлайн обычный Инженерный калькулятор онлайн Замена русских букв на английские для вебмастеров Замена русских букв на английские

Аппаратное и программное обеспечение Графика и компьютерная сфера Интегрированная геоинформационная система Интернет Компьютер Комплектующие компьютера Лекции Методы и средства измерений неэлектрических величин Обслуживание компьютерных и периферийных устройств Операционные системы Параллельное программирование Проектирование электронных средств Периферийные устройства Полезные ресурсы для программистов Программы для программистов Статьи для программистов Cтруктура и организация данных


 


Не нашли то, что искали? Google вам в помощь!

 
 

© life-prog.ru При использовании материалов прямая ссылка на сайт обязательна.