Cтраница 2
Он построил около полудюжины простых хорновских дизъюнктов, представляющих необходимый механизм УМТ, и доказал затем, что любая вычислимая по Тьюрингу функция может быть вычислена с помощью резолюции, исходя из этих дизъюнктов в ответ на соответствующие целевые утверждения. Кроме того, хорошо известный факт о том, что не существует никакого алгоритма, позволяющего решить, закончится или нет произвольное тьюрингово вычисление ( проблема остановки), преобразуется тогда в эквивалентный факт: не существует никакого алгоритма, позволяющего решить, дает ли произвольная программа на хорновских дизъюнктах конечное успешное резолютивное вычисление. Это в свою очередь просто вариант того факта, что общезначимость произвольных предложений в логике первого порядка не является полностью разрешимой. [16]
Наши знания формально представляются хорновскими дизъюнктами, которые не только позволяют описывать в простых терминах события окружающего мира, но и легко преобразуются в сколемов-скую стандартную форму. Аппарат вывода с подстановкой, унификацией и резолюцией, задействованный в нашем языке, предоставляет удобное алгоритмическое средство для обработки данных и извлечения заключений из множества хорновских дизъюнктов. [17]
Такие формулы и называются хорновскими дизъюнктами, а стиль программирования - хорновским. [18]
Каждое правило грамматики интерпретируется как хорновский дизъюнкт. Множество таких дизъюнктов представляет грамматику как множество гипотез, необходимых для доказательства некой логической теоремы, например: данный список слов есть фраза языка. Более строго: данный список слов есть логическое следствие правил грамматики. [19]
Мы увидим, что преимущество хорновских дизъюнктов при поиске вывода методом резолюции заключается в наличии единственного входа - положительной литеры при поиске партнера для применения резолюции к отрицательной литере. Это приводит к систематическому методу поиска в глубину слева направо при попытках применять резолюцию и производить подстановки; этот метод напоминает программирование с бектрекингом. [20]
Резолюционная интерпретация Пролога с использованием хорновских дизъюнктов ограничена в следующем отношении. Ни на каком шаге резолюция не применяется к текущему, только что полученному дизъюнкту и некоторому ранее выведеному дизъюнкту. [21]
ПРОЛОГ просматривает данные в поисках хорновского дизъюнкта, заголовок которого может быть унифицирован с текущей целью. ПГОЛОГ тут же пытается проверить тело формулы ( 11), объявляя текущими целями одну за другой все посылки этой формулы. [22]
Теорема 1.6. Любое конечное выполнимое множество хорновских дизъюнктов допускает одну и только одну минимальную модель. [23]
Является ли данная формула исчисления предикатов хорновским дизъюнктом. [24]
Этот алгоритм, применимый только к множеству хорновских дизъюнктов, очень похож на общий алгоритм из § 1.1.13. Принципиальное отличие состоит в том, что на каждом этапе некая литера удаляется из одного дизъюнкта. Отсюда сразу же следует, что выполнение алгоритма всегда завершается, какая бы стратегия ни была принята при выборе рис. Если N - число литер, первоначально присутствующих в S ( с учетом повторений), то цикл будет выполняться не более N раз. [25]
Эти недостатки связаны не только с ограниченностью процедуры вывода ( хорновские дизъюнкты, неполная входная резолюция, поиск только в глубину, порядок разрешения литер), но также и с тем, что языки логического программирования на сегодняшний день ориентированы, главным образом, на фон-неймановскую архитектуру машин, что, конечно, является недостаточным для создания принципиально новых образцов вычислительной техники. [26]
Имеются в виду, конечно, резолютивные доказательства из множеств хорновских дизъюнктов. Если же мы будем доказывать существование исходя из произвольной спецификации S, то резолютивный вывод может оказаться неконструктивным и решения не дать. [27]
Отметим, что для приведенного примера, состоящего из восьми хорновских дизъюнктов, дерево поиска имеет достаточно большую размерность. Отсюда возникает задача: как найти все альтернативные решения, представляющие композиции подстановок, используемых на пути от корневой вершины к пустой; или, иначе говоря, как найти все пути, идущие от корневой вершины к пустым. [28]
Сформулируйте следующие высказывания, данные на обыденном языке, в виде хорновских дизъюнктов. [29]
SL-резолюцией для дефинициалъных ( definite) дизъюнктов, где под дефинициальным дизъюнктом понимают хорновский дизъюнкт. [30]