У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

Тут можно читать онлайн У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ - бесплатно полную версию книги (целиком) без сокращений. Жанр: comp-programming. Здесь Вы можете читать полную версию (весь текст) онлайн без регистрации и SMS на сайте лучшей интернет библиотеки ЛибКинг или прочесть краткое содержание (суть), предисловие и аннотацию. Так же сможете купить и скачать торрент в электронном формате fb2, найти и слушать аудиокнигу на русском языке или узнать сколько частей в серии и всего страниц в публикации. Читателям доступно смотреть обложку, картинки, описание и отзывы (комментарии) о произведении.
  • Название:
    ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ
  • Автор:
  • Жанр:
  • Издательство:
    неизвестно
  • Год:
    неизвестен
  • ISBN:
    нет данных
  • Рейтинг:
    3.7/5. Голосов: 101
  • Избранное:
    Добавить в избранное
  • Отзывы:
  • Ваша оценка:
    • 80
    • 1
    • 2
    • 3
    • 4
    • 5

У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ краткое содержание

ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ - описание и краткое содержание, автор У Клоксин, читайте бесплатно онлайн на сайте электронной библиотеки LibKing.Ru

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

ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ - читать онлайн бесплатно полную версию (весь текст целиком)

ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ - читать книгу онлайн бесплатно, автор У Клоксин
Тёмная тема
Сбросить

Интервал:

Закладка:

Сделать

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

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

:-.

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

Каким образом это свойство метода резолюций может помочь нам? Имеет место следующий факт:

Если множество формул { А 1, A 2,…, А n } совместно, то формула Вявляется следствием формул { A l ,A 2,…, A n } тогда и только тогда, когда множество формул { А 1, A 2,…, А nВ } - несовместно.

Таким образом, если множество гипотез совместно, то необходимо лишь добавить к нему дизъюнкты, соответствующие отрицанию высказывания, которое следует доказать. Резолюция даст пустой дизъюнкт в точности тогда, когда доказываемое высказывание следует из данных гипотез. Дизъюнкты, добавляемые к множеству гипотез, называются целевыми дизъюнктами. Отметим, что целевые дизъюнкты ничем не отличаются от гипотез – и те и другие являются дизъюнктами. Так что, если задано множество дизъюнктов { А 1, А 2, …, А п } и требуется проверить несовместность этого множества дизъюнктов, то в действительности невозможно определить, идет ли речь о доказательстве того, что ⌉ А 1 следует из A 2, А 3, …, А п или что ⌉ А 2следует из A 1, A 3, , А n, или что ⌉ А 3 следует из А 1, А 2, A 4,…, А nи так далее. Именно это является причиной того, что необходимо указывать какие дизъюнкты в действительности являются целевыми дизъюнктами. Для системы, использующей метод резолюций, все перечисленные задачи эквивалентны.

Легко увидеть, как можно получить пустой дизъюнкт в примере с королем Артуром, если добавить целевой дизъюнкт:

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

(это дизъюнкт для ~король(артур)). Ранее уже было показано, как дизъюнкт

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

может быть выведен из гипотез. Применяя правило резолюций к (5) и (6) (сопоставляя любую из атомарных формул в (5)), получаем:

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

И наконец, резолюция дизъюнктов (6) и (7) дает

:-.

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

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

На решение этих вопросов направлено много различных улучшений исходного принципа резолюций. В следующем разделе рассматриваются некоторые из них.

10.5. Хорновские дизъюнкты

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

Прежде всего, очевидно, что существуют два вида хорнов-ских дизъюнктов – дизъюнкты, содержащие один литерал без отрицания и дизъюнкты, не содержащие таких литералов. Будем называть эти два типа хорновских дизъюнктов соответственно дизъюнктами с заголовком и дизъюнктами без заголовка. Следующие примеры иллюстрируют указанные типы дизъюнктов (необходимо помнить, что литералы без отрицания записываются слева от знака ':-'):

Читать дальше
Тёмная тема
Сбросить

Интервал:

Закладка:

Сделать


У Клоксин читать все книги автора по порядку

У Клоксин - все книги автора в одном месте читать по порядку полные версии на сайте онлайн библиотеки LibKing.




ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ отзывы


Отзывы читателей о книге ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ, автор: У Клоксин. Читайте комментарии и мнения людей о произведении.


Понравилась книга? Поделитесь впечатлениями - оставьте Ваш отзыв или расскажите друзьям

Напишите свой комментарий
x