Шрифт:
В 60-х годах в этой области наблюдалась большая активность, связанная с возможностью использования вычислительных машин для автоматического доказательства теорем. Именно эта область научной деятельности, по-прежнему остающаяся источником новых идей и методов, дала жизнь идеям, легшим в основу Пролога. Одним из фундаментальных достижений того времени явилось открытие Дж. А. Робинсоном принципа резолюцийи его применение к автоматическому доказательству теорем. Резолюция – это правило вывода,говорящее о том, как одно высказывание может быть получено из других. Используя принцип резолюций, можно полностью автоматически доказывать теоремы, выводя их из аксиом. Необходимо лишь решать, к каким из высказываний следует применять правило вывода, а правильные следствия из них будут строиться автоматически.
Правило резолюций разрабатывалось применительно к формулам, представленным в стандартной форме. Если заданы два дизъюнкта, связанных между собой определенным образом, то это правило породит новый дизъюнкт, являющийся следствием двух первых. Главная идея состоит в том, что, если одна и та же атомарная формула появляется как в левой части одного дизъюнкта, так и в правой части другого дизъюнкта, то дизъюнкт, получаемый в результате соединения этих двух дизъюнктов, из которых вычеркнута упоминавшаяся повторяющаяся формула, является следствием указанных дизъюнктов. Например,
Из
унылый(крист); сердитый(крис):- рабочий_день(сегодня), идет_дождь(сегодня).
и
неприятный(крис):- сердитый(крис), усталый(крис).
следует
унылый(крис); неприятный(крис):- рабочий_день(сегодня), идет_дождь(сегодня), усталый(крис).
На естественном языке это звучит так. Если сегодня рабочий день и идет дождь, то Крис – унылый или сердитый. Кроме того, если Крис сердитый и усталый, то он неприятен. Поэтому, если сегодня рабочий день, идет дождь и Крис усталый, то Крис является унылым или неприятным.
В действительности, мы сильно упростили ситуацию, опустив два момента. Прежде всего, ситуация усложняется, когда дизъюнкты содержат переменные. В такой ситуации две атомарные формулы не обязательно должны быть идентичными – они должны быть лишь «сопоставимы». Кроме того, дизъюнкт, являющийся следствием двух других дизъюнктов, получается в результате их соединения (с удалением повторяющейся формулы) с помощью некоторой дополнительной операции. Эта операция включает в себя«конкретизацию» переменных до такой степени, чтобы две сопоставляемые формулы стали идентичными. Используя терминологию Пролога, можно сказать, что, если имелось два дизъюнкта, представленных в виде структур, и было выполнено сопоставление соответствующих подструктур, то результат соединения этих структур и был бы представлением нового дизъюнкта. Второе упрощение состоит в том, что в общем случае, правило резолюций допускает сопоставление нескольких литералов в правой части одного дизъюнкта с несколькимилитералами в левой части другого дизъюнкта. Здесь будут рассматриваться лишь примеры, когда из каждого дизъюнкта выбирается один литерал.
Рассмотрим один пример применения правила резолюций при наличии переменных:
человек(f1(Х)); король(Х):-. (1)
король(Y):- почитает(f1(Y),Y). (2)
почитает(Z,артур):- человек(Y). (3)
Два первых дизъюнкта представляют стандартную форму формулы, которую можно выразить так: «если каждый человек почитает кого-то, то этот кто-то – король». Переменные переименованы для удобства объяснения. Третий дизъюнкт выражает высказывание о том, что каждый человек почитает Артура. Применяя правило резолюций к (2) и (3) (сопоставляя два соответствующих литерала), получаем:
король(артур):- человек(f1(артур)). (4)
( Yв (2) сопоставлен с артурв (3), a Zв (3) сопоставлен с fl(Y)в (2)). Теперь можно применить правило резолюций к (1) и (4), что дает:
король(артур); король(артур):-.
Это эквивалентно факту, гласящему, что Артур является королем.
В формальном определении метода резолюций процедура «сопоставления», на которую мы неформально ссылались, называется унификацией.Интуитивно, множество атомарных формул унифицируемо,если эти формулы могут быть сопоставлены друг с другом как структуры языка Пролог. В действительности, как это будет показано в одном из следующих разделов, процедура сопоставления, используемая в большинстве реализаций языка Пролог, не совпадает в точности с унификацией.
Как можно использовать метод резолюций для доказательства конкретных утверждений? Один из возможных способов состоит в том, чтобы последовательно, шаг за шагом, применять правило резолюций к имеющимся гипотезам и посмотреть, не появилось ли при этом то, что мы хотим доказать. К сожалению, нельзя гарантировать, что это в конце концов произойдет, даже если интересующее нас высказывание действительно следует из имеющихся гипотез. Так, например, в последнем примере нельзя вывести простой дизъюнкт король(артур), исходя из данного множества дизъюнктов и используя лишь указанный метод, несмотря даже на то, что это очевидное следствие. Следует ли отсюда, что метод резолюций не является достаточно мощным средством для наших целей? К счастью, ответом на этот вопрос является «нет», так как можно переформулировать постановку задачи таким образом, что метод резолюций гарантированно сможет решить ее, если это в принципе возможно.
Метод резолюций имеет одно важное формальное свойство – он является полным для доказательства несовместности множества дизъюнктов.Это значит, что если множество дизъюнктов несовместно,то используя метод резолюций всегда можно вывести из данного множества дизъюнктов пустой дизъюнкт:
:-.
Кроме того, так как метод резолюций является корректным,то единственное, что он может вывести в такой ситуации – это пустой дизъюнкт. Множество формул несовместно, если не существует интерпретации предикатов, констант и функциональных символов, делающей истинными одновременно все эти формулы. Пустой дизъюнкт является логическим выражением ложности– он представляет высказывание, которое ни при каких условиях не может быть истинным. Таким образом, метод резолюций наверняка определит, когда заданное множество формул является несовместным, выведя пустой дизъюнкт, являющийся выражением противоречия.
Жанры
- Романы
- Приключения
- Детективы
- Техно триллер
- Дамский детективный роман
- Исторические детективы
- Классические детективы
- Шпионские детективы
- Триллеры
- Юридический триллер
- Крутой детектив
- Полицейские детективы
- Медицинский триллер
- Иронические детективы
- Боевики
- Криминальные детективы
- Политические детективы
- Маньяки
- Зарубежные детективы
- Прочие Детективы
- Спецслужбы
- Драматургия
- Фантастика
- Хентай
- Ранобэ
- Сянься
- Дорама
- Уся
- Аниме
- Космоопера
- Юмористическая фантастика
- Боевая фантастика
- Героическая фантастика
- Технофэнтези
- Готический роман
- Социально-философская фантастика
- Попаданцы
- Историческая фантастика
- Ироническая фантастика
- Зарубежная фантастика
- Историческое фэнтези
- Юмористическое фэнтези
- Детективная фантастика
- Эпическая фантастика
- Мистика
- Космическая фантастика
- Фантастика: прочее
- Постапокалипсис
- Научная фантастика
- Киберпанк
- Альтернативная история
- Ненаучная фантастика
- РПГ
- Стимпанк
- Ироническое фэнтези
- Ужасы и мистика
- Сказочная фантастика
- Фэнтези
- Городское фэнтези
- Эзотерика
- Проза
- Военная проза
- Легкая проза
- Сентиментальная проза
- Советская классическая проза
- Антисоветская литература
- Афоризмы
- Эпистолярная проза
- Новелла
- Семейный роман
- Рассказ
- Классическая проза
- Эпопея
- Эссе
- Проза прочее
- Повесть
- Магический реализм
- Современная проза
- Контркультура
- Роман
- Историческая проза
- Русская классическая проза
- Феерия
- Стихи и поэзия
- Юмор
- Дом и досуг
- Рыбалка
- Охота
- Здоровье детей
- Домашние животные
- Воспитание детей
- Отдых / туризм
- Зарубежная прикладная литература
- Прочее домоводство
- Прикладная литература
- Домашнее хозяйство
- Кулинария
- Медицина и здоровье
- Сделай сам
- Спорт
- Хобби и ремесла
- Образовательная литература
- Сад и Огород
- Здоровье и красота
- Развлечения
- Коллекционирование
- Секс / секс-руководства
- Образование и наука
- Боевые искусства
- Органическая химия
- Обществознание
- Военная история
- Ветеринария
- Ораторское искусство / риторика
- Физика
- Химия
- Семейная психология
- Военная техника и вооружение
- Иностранные языки
- Прочая научная литература
- Психотерапия и консультирование
- Биохимия
- Cпецслужбы
- Астрономия и Космос
- Школьные учебники
- Учебная и научная литература
- Учебники
- Государство и право
- Психология
- Литературоведение
- История
- Научно-популярная литература
- Политика
- Детская психология
- Юриспруденция
- Шпаргалки
- Педагогика
- Физическая химия
- Медицина
- Биофизика
- Языкознание
- Зарубежная образовательная литература
- Зоология
- Геология и география
- Краткое содержание
- Зарубежная психология
- Саморазвитие / личностный рост
- Технические науки
- Религиоведение
- Военное дело
- Личная эффективность
- Аналитическая химия
- Рефераты
- Экология
- Философия
- Альтернативная медицина
- Математика
- Культурология
- Военное дело: прочее
- Ботаника
- Биология
- Словари и Энциклопедии
- Финансы и бизнес
- Отраслевые издания
- Бухучет и аудит
- Недвижимость
- Деловая литература
- Ценные бумаги
- Внешнеэкономическая деятельность
- Торговля
- Зарубежная деловая литература
- О бизнесе популярно
- Стартапы и создание бизнеса
- Корпоративная культура
- Управление, подбор персонала
- Маркетинг, PR, реклама
- Личные финансы
- Работа с клиентами
- Менеджмент
- Интернет-бизнес
- Поиск работы, карьера
- Малый бизнес
- Делопроизводство
- Государственное и муниципальное управление
- Банковское дело
- Экономика
- Книги по IT
- Техника
- Древние книги
- Документальное
- Прочее
- Интерьеры
- Газеты и журналы
- Театр
- Музыка
- Комиксы / манга
- Зарубежная классика
- Современная зарубежная литература
- Изобразительное искусство, фотография
- Мода и стиль
- Искусство и Дизайн
- Зарубежная литература о культуре и искусстве
- Фанфик
- Подростковая литература
- Шахматы
- Кино
- Культура и искусство
- Недописанное
- Классическая литература
- Без Жанра
- Народные
- Книги Для Детей
- Детские остросюжетные
- Сказки
- Детские стихи
- Прочая детская литература
- Детская образовательная литература
- Книги для дошкольников
- Детская фантастика
- Детские детективы
- Книга-игра
- Детский фольклор
- Буквари
- Детская проза
- Детская познавательная и развивающая литература
- Внеклассное чтение
- Зарубежные детские книги
- Детские приключения