Вход/Регистрация
Программирование на языке пролог
вернуться

Клоксин У.

Шрифт:

В 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), что дает:

король(артур); король(артур):-.

Это эквивалентно факту, гласящему, что Артур является королем.

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

Как можно использовать метод резолюций для доказательства конкретных утверждений? Один из возможных способов состоит в том, чтобы последовательно, шаг за шагом, применять правило резолюций к имеющимся гипотезам и посмотреть, не появилось ли при этом то, что мы хотим доказать. К сожалению, нельзя гарантировать, что это в конце концов произойдет, даже если интересующее нас высказывание действительно следует из имеющихся гипотез. Так, например, в последнем примере нельзя вывести простой дизъюнкт король(артур), исходя из данного множества дизъюнктов и используя лишь указанный метод, несмотря даже на то, что это очевидное следствие. Следует ли отсюда, что метод резолюций не является достаточно мощным средством для наших целей? К счастью, ответом на этот вопрос является «нет», так как можно переформулировать постановку задачи таким образом, что метод резолюций гарантированно сможет решить ее, если это в принципе возможно.

Метод резолюций имеет одно важное формальное свойство – он является полным для доказательства несовместности множества дизъюнктов.Это значит, что если множество дизъюнктов несовместно,то используя метод резолюций всегда можно вывести из данного множества дизъюнктов пустой дизъюнкт:

:-.

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

  • Читать дальше
  • 1
  • ...
  • 89
  • 90
  • 91
  • 92
  • 93
  • 94
  • 95
  • 96
  • 97
  • 98
  • 99
  • ...
Жанры
  • Романы
    • Исторические любовные романы
    • Эро литература
    • Современные любовные романы
    • Короткие любовные романы
    • Love Action
    • Остросюжетные любовные романы
    • Романы про измену
    • Прочие любовные романы
    • Любовно-фантастические романы
    • Зарубежные любовные романы
  • Приключения
    • Прочие приключения
    • Вестерны
    • Исторические приключения
    • Морские приключения
    • Путешествия и география
    • Зарубежные приключения
    • Приключения про индейцев
    • Природа и животные
  • Детективы
    • Техно триллер
    • Дамский детективный роман
    • Исторические детективы
    • Классические детективы
    • Шпионские детективы
    • Триллеры
    • Юридический триллер
    • Крутой детектив
    • Полицейские детективы
    • Медицинский триллер
    • Иронические детективы
    • Боевики
    • Криминальные детективы
    • Политические детективы
    • Маньяки
    • Зарубежные детективы
    • Прочие Детективы
    • Спецслужбы
  • Драматургия
    • Водевиль
    • Драма
    • Киносценарии
    • Мистерия
    • Пьесы
    • Сценарии
    • Трагедия
    • Зарубежная драматургия
  • Фантастика
    • Хентай
    • Ранобэ
    • Сянься
    • Дорама
    • Уся
    • Аниме
    • Космоопера
    • Юмористическая фантастика
    • Боевая фантастика
    • Героическая фантастика
    • Технофэнтези
    • Готический роман
    • Социально-философская фантастика
    • Попаданцы
    • Историческая фантастика
    • Ироническая фантастика
    • Зарубежная фантастика
    • Историческое фэнтези
    • Юмористическое фэнтези
    • Детективная фантастика
    • Эпическая фантастика
    • Мистика
    • Космическая фантастика
    • Фантастика: прочее
    • Постапокалипсис
    • Научная фантастика
    • Киберпанк
    • Альтернативная история
    • Ненаучная фантастика
    • РПГ
    • Стимпанк
    • Ироническое фэнтези
    • Ужасы и мистика
    • Сказочная фантастика
    • Фэнтези
    • Городское фэнтези
  • Эзотерика
    • Язычество
    • Фэн-шуй
    • Христианство
    • Религия
    • Зарубежная религиозная литература
    • Православие
    • Эзотерика
    • Хиромантия
    • Индуизм
    • Ислам
    • Протестантизм
    • Самосовершенствование
    • Буддизм
    • Католицизм
    • Астрология
    • Прочая религиозная литература
    • Иудаизм
  • Проза
    • Военная проза
    • Легкая проза
    • Сентиментальная проза
    • Советская классическая проза
    • Антисоветская литература
    • Афоризмы
    • Эпистолярная проза
    • Новелла
    • Семейный роман
    • Рассказ
    • Классическая проза
    • Эпопея
    • Эссе
    • Проза прочее
    • Повесть
    • Магический реализм
    • Современная проза
    • Контркультура
    • Роман
    • Историческая проза
    • Русская классическая проза
    • Феерия
  • Стихи и поэзия
    • Визуальная поэзия
    • Эпическая поэзия
    • в стихах
    • Песенная поэзия
    • Поэзия
    • Палиндромы
    • Cтихи, поэзия
    • Зарубежная поэзия
    • Верлибры
    • Экспериментальная поэзия
    • Лирика
    • Басни
    • Драматургия
  • Юмор
    • Зарубежный юмор
    • Юмористические стихи
    • Сатира
    • Прочий юмор
    • Комедия
    • Юмористическая проза
    • Анекдоты
  • Дом и досуг
    • Рыбалка
    • Охота
    • Здоровье детей
    • Домашние животные
    • Воспитание детей
    • Отдых / туризм
    • Зарубежная прикладная литература
    • Прочее домоводство
    • Прикладная литература
    • Домашнее хозяйство
    • Кулинария
    • Медицина и здоровье
    • Сделай сам
    • Спорт
    • Хобби и ремесла
    • Образовательная литература
    • Сад и Огород
    • Здоровье и красота
    • Развлечения
    • Коллекционирование
    • Секс / секс-руководства
  • Образование и наука
    • Боевые искусства
    • Органическая химия
    • Обществознание
    • Военная история
    • Ветеринария
    • Ораторское искусство / риторика
    • Физика
    • Химия
    • Семейная психология
    • Военная техника и вооружение
    • Иностранные языки
    • Прочая научная литература
    • Психотерапия и консультирование
    • Биохимия
    • Cпецслужбы
    • Астрономия и Космос
    • Школьные учебники
    • Учебная и научная литература
    • Учебники
    • Государство и право
    • Психология
    • Литературоведение
    • История
    • Научно-популярная литература
    • Политика
    • Детская психология
    • Юриспруденция
    • Шпаргалки
    • Педагогика
    • Физическая химия
    • Медицина
    • Биофизика
    • Языкознание
    • Зарубежная образовательная литература
    • Зоология
    • Геология и география
    • Краткое содержание
    • Зарубежная психология
    • Саморазвитие / личностный рост
    • Технические науки
    • Религиоведение
    • Военное дело
    • Личная эффективность
    • Аналитическая химия
    • Рефераты
    • Экология
    • Философия
    • Альтернативная медицина
    • Математика
    • Культурология
    • Военное дело: прочее
    • Ботаника
    • Биология
  • Словари и Энциклопедии
    • Бизнес-справочники
    • Справочники
    • Словари
    • Руководства
    • Энциклопедии
    • Словари, справочники
    • Путеводители
    • Прочая справочная литература
    • Зарубежная справочная литература
  • Финансы и бизнес
    • Отраслевые издания
    • Бухучет и аудит
    • Недвижимость
    • Деловая литература
    • Ценные бумаги
    • Внешнеэкономическая деятельность
    • Торговля
    • Зарубежная деловая литература
    • О бизнесе популярно
    • Стартапы и создание бизнеса
    • Корпоративная культура
    • Управление, подбор персонала
    • Маркетинг, PR, реклама
    • Личные финансы
    • Работа с клиентами
    • Менеджмент
    • Интернет-бизнес
    • Поиск работы, карьера
    • Малый бизнес
    • Делопроизводство
    • Государственное и муниципальное управление
    • Банковское дело
    • Экономика
  • Книги по IT
    • Прочая компьютерная литература
    • Базы данных
    • Цифровая обработка сигналов
    • Программное обеспечение
    • Интернет
    • Программирование
    • Зарубежная компьютерная литература
    • ОС и Сети
    • Компьютерное «железо»
  • Техника
    • Архитектура
    • Автомобили и ПДД
    • Строительство и сопромат
    • Металлургия
    • Транспорт и авиация
    • Радиоэлектроника
  • Древние книги
    • Зарубежная старинная литература
    • Мифы. Легенды. Эпос
    • Древневосточная литература
    • Древнерусская литература
    • Прочая старинная литература
    • Античная литература
    • Европейская старинная литература
  • Документальное
    • Историческая литература
    • Публицистика
    • Научпоп
    • Критика
    • Книги о войне
    • Истории из жизни
    • Военная документалистика
    • Зарубежная публицистика
    • Биографии и мемуары
    • Прочая документальная литература
  • Прочее
    • Интерьеры
    • Газеты и журналы
    • Театр
    • Музыка
    • Комиксы / манга
    • Зарубежная классика
    • Современная зарубежная литература
    • Изобразительное искусство, фотография
    • Мода и стиль
    • Искусство и Дизайн
    • Зарубежная литература о культуре и искусстве
    • Фанфик
    • Подростковая литература
    • Шахматы
    • Кино
    • Культура и искусство
    • Недописанное
    • Классическая литература
  • Без Жанра
    • Разное
    • Иностранная литература
  • Народные
    • Загадки
    • Народные сказки
    • Народные песни
    • Былины
    • Частушки
    • Фольклор: прочее
    • Пословицы, поговорки
  • Книги Для Детей
    • Детские остросюжетные
    • Сказки
    • Детские стихи
    • Прочая детская литература
    • Детская образовательная литература
    • Книги для дошкольников
    • Детская фантастика
    • Детские детективы
    • Книга-игра
    • Детский фольклор
    • Буквари
    • Детская проза
    • Детская познавательная и развивающая литература
    • Внеклассное чтение
    • Зарубежные детские книги
    • Детские приключения
Сейчас Читают
Para bellum
Para bellum
Ланцов Михаил Алексеевич
Прометей: повелитель стали
Прометей: повелитель стали
Рави Ивар
Мама для дракончика или Жена к вылуплению
Мама для дракончика или Жена к вылуплению
Максонова Мария
Моя (не) на одну ночь. Бесконтрактная любовь
Моя (не) на одну ночь. Бесконтрактная любовь
Тоцка Тала
Маверик
Маверик
Астахов Евгений Евгеньевич
Я же бать, или Как найти мать
Я же бать, или Как найти мать
Юнина Наталья
Без Чести
Без Чести
Щукин Иван
Генерал Скала и ученица
Генерал Скала и ученица
Суббота Светлана
Провинциал. Книга 4
Провинциал. Книга 4
Лопарев Игорь Викторович
Мастер 6
Мастер 6
Чащин Валерий

Ебукер (ebooker) – онлайн-библиотека на русском языке. Книги доступны онлайн, без утомительной регистрации. Огромный выбор и удобный дизайн, позволяющий читать без проблем. Добавляйте сайт в закладки! Все произведения загружаются пользователями: если считаете, что ваши авторские права нарушены – используйте форму обратной связи.

Полезные ссылки

  • Моя полка

Контакты

  • chitat.ebooker@gmail.com

Подпишитесь на рассылку: