Интеллектуальные информационные системы. Дубровин А.Д. - 77 стр.

приведение не противоречит исходной структуре), так чтобы один операнд был заведомо истинным или ложным.
Затем применяется одно из аксиоматических правил дедуктивного вывода и на его основе делается
результирующий вывод.
          Доказательство «от противного» основано на том, что вместо высказывания, которое надо доказать,
формулируется противоречивое ему высказывание, которое и доказывается. Если противоречивое высказывание
окажется истинным, то исходное должно быть ложным, и – наоборот. Противоречие может быть выражено либо
по форме, либо по содержанию. Противоречие по форме предполагает выбор новой формулировки, но с теми же
логическими значениями операндов. Противоречие по содержанию предполагает сохранение формулировки
исходного предиката с заменой логических значений операндов на противоположные.
           Доказательство с применением «метода резолюций» более сложно. Оно основано на применении
теоремы (тавтологии), формула которой представляет собой импликацию вида
                        ((А∨Х) ∧ (В∨(¬Х)))→(А∨В).
      Посылкой в этой импликации (ее первым операндом) является конъюнкция двух дизъюнкций. В правой
дизъюнкции переменная Х представлена ее отрицанием (¬Х).Коль скоро тавтология по определению имеет
логическое значение «И» при любых значениях операндов, остается привести высказывание, которое требуется
доказать к виду этой «резолюции» и задача решена. Реализуется метод достаточно просто, в связи с тем, что
конструкция тавтологии является как бы «наибольшим общим делителем» для практически любых
формулировок многоместных предикатов. Фрагмент таблицы истинности для «правила резолюции» приведен
ниже.

                                                         Таблица 3.2.2



           А    В    А∨В      Х     А∨Х       В∨(¬Х)      (А∨Х)∧(В∨(¬Х)     вывод

           И    И      И      И       И         И               И              И

           И    Л      И     И        И         Л               Л              И

           Л    И      И     И        И         И               И              И

           Л    Л     Л      И        И         Л              Л               И




         Метод резолюции хорош тем, что он легко реализуется и является достаточно универсальным для
исчисления предикатов.
            Для машинного решении подобных задач должны быть автоматически выполнены все атрибутивные
процедуры: приведение к безизбыточности, вынесение за скобки кванторов, исключение тавтологий и пр.
            Применение формально-логических моделей представления знаний потребовало создания
процедурных языков программирования, таких как PROLOG. Программирование на нем системы логических
выводов позволяет реализовать все атрибутивные процедуры метода резолюции в три этапа:
         - описание свойств объектов и отношений между ними;
         - определение правил, на основании которых могут образовываться различные типы отношений;
         - определение правил формулирования вопросов о свойствах объектов и отношениях между ними.
            Формально-логические модели более эффективно применяются там, где решение задач идет на
абстрактном уровне – то есть, в научно исследовательских и теоретических системах. Применение этого типа
моделей ПЗ в сферах промышленного производства или в системах управления сложными структурами не может
дать приемлемого результата из-за сложности применения таких моделей, из-за жестких требований к
оперативности получения новых знаний и большого объема БЗ в системах, модели которых предусматривают не
только абстракции, но и реальные объекты.




                                                                                                     81