Принцип резолюции в исчислении высказываний и логике предикатов и его модификации

     P1, ..., Рт <— q1,...qn содержит переменные  х1,..., хk, то правильная интерпретация  имеет следующий вид:

     для всех x1, ..., хk

     p1 или ... или pm является истинным, если q1 и ... и qn являются истинными.

     Если  п = 0, т.е. отсутствует хотя бы одно условие, то выражение будет интерпретироваться следующим образом:

     для всех x1, ..., xk

     p1 или ... или рт является истинным.

     Если  т = 0, т.е. отсутствуют термы заключения, то выражение будет интерпретироваться следующим образом:

     для всех x1, ..., xk

     не  имеет значения, что q1 и ... и qn являются истинными.

     Если  же т = п = 0, то мы имеем дело с пустой фразой, которая всегда интерпретируется как ложная. 

     3.2 Программирование на ПРОЛОГЕ. 

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

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

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

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

     Фразы Хорна (Horn clause) представляют собой подмножество фраз, содержащих только один позитивный литерал. В общем виде фраза Хорна  представляется выражением

     В языке PROLOG эта же фраза записывается в таком виде:

     р :- q1,...,qn. Такая фраза интерпретируется следующим образом:

     "Для  всех значений переменных в  фразе p истинно, если истинны  q1 и ... и qn",

     т.е. пара символов ":-" читается как "если", а запятые читаются как "и".

     PROLOG — это не совсем обычный  язык программирования, в котором  программа состоит в основном  из логических формул, а процесс  выполнения программы представляет  собой доказательство теоремы  определенного вида.

     Фраза в форме

     р :- q1, ...,qn.

     может рассматриваться в качестве процедуры. Такая процедура предполагает следующий порядок выполнения операций.

     (1) Литерал цели сопоставляется  с литералом р (унифицируется  с р), который называется головой  фразы.

     (2)Хвост  фразы ql, ...,qn конкретизируется подстановкой значений переменных (или унификаторов), сформированных в результате этого сопоставления.

     (3) Конкретизированные термы хвостовой  части образуют затем множество  подцелей, которые могут быть  использованы другими процедурами.

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

     Например, рассмотрим набор фраз языка PROLOG, представленных в листинге 1. Предположим, что a, b и с — какие-то блоки в мире блоков. Две первые фразы утверждают, что а находится на (on) b, a b находится на (on) с. Третья фраза утверждает, что X находится выше (above) Y, если X находится на (on) Y. Четвертая фраза утверждает, что X находится выше (above) Y, если существует какой-то другой блок Z, размещенный на (on) Y, и X находится выше (above) Y. 

     Листинг 1. Простая программа на языке PROLOG, определяющая отношение 

     on (на)

     on(а, b).

     on(b, с).

     above(X, Y) :- on(X, Y).

     above(X, Y) :- on(Z, Y),

     above(X, Z). 

     Очевидно, что от программы требуется вывести цель above (а, с) из этого множества фраз. Процесс формулировки выражения цели включает обработку двух процедур above и использование двух фраз on. В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation). 

     3.3 Принцип резолюций 

     Мы  стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]).

     Рассмотрим  следующий пример из исчисления высказываний. В дальнейшем прописными буквами  Р, Q, R,... будут обозначаться отдельные  фразы, а строчными греческими U, ф и Ј — пропозициональные  переменные, как и раньше.

     Если U и ф представляют две произвольные фразы, которые можно представить в конъюнктивной нормальной форме, и

     U={ U1, ..., Ui, ...., Um},

     и

     ф= {ф1..., фi.....,фn}, и

     Ui, = ¬фi при 1[i[mm,1 [j [ n,

     то  новую фразу Ј можно вывести  из объединения U' и ф', где

     U' = U¬{ Ui} и ф' = ф¬{ф,}.

     Фраза Ј = U' и ф' называется резольвентой шага резолюции, а U и ф являются родительскими  фразами. Иногда говорят, что U и ф "сталкиваются" на паре дополняющих литералов Ui , и  фj.

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

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

     Таблица 1. Обобщение резолюции. 

 

     Противоречие в правиле, которое обычно обозначается значком 1, дает в результате пустую фразу— {}. Это означает, что предпосылки несовместимы. Если считать, что предпосылки описывают некоторое состояние предметной области, то такой набор предпосылок не может быть реально обеспечен в ней, т.е. такое состояние невозможно.

     Главное, что компонент автоматического  доказательства теорем, который является основным компонентом большинства  систем искусственного интеллекта и, в  частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.

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

     Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода. 

     3.4 Поиск доказательства в системе резолюций 

     Резолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорится о том, как выполнить доказательство. Обратим основное внимание на стратегические аспекты доказательства теорем.

     Пусть р представляет утверждение "Сократ — это человек", a q — утверждение "Сократ смертен". Пусть наша теория имеет вид

     Т={{¬р,q}, {р}}.

     Таким образом, утверждается, что если Сократ человек, то Сократ смертен, и что Сократ — человек. {17} выводится из теории Т за один шаг резолюции, эквивалентной правилу modus ponens. .

     Выражения {¬р, q} и {р} "сталкиваются" на паре дополняющих литералов р и  ¬р, а {q} является резольвентой. Таким  образом, теория Алогически подразумевает д, что записывается в форме Т|-q. Теперь можно добавить новую фразу {q} — резольвенту — в теорию Т и получить таким образом теорию

     Т'= {{ ¬ip, q}, {p}, {q}}.

     Конечно, в большинстве случаев для  доказательства требуется множество  шагов. Положим, например, что теория Т имеет вид

     В этой теории р и q сохраняют прежний  смысл, а г представляет утверждение "Сократ — бог". Для того чтобы  показать, что Т|- ¬r , потребуются  два шага резолюции:

     {¬q,p},{Р}/{q}

     {¬q,-r},{q} / {-r}

     Обратите  внимание, что на первом шаге используются две фразы из исходного множества Т, а на втором— резольвента {q}, добавленная к Т. Кроме того, следует отметить, что доказательство может быть выполнено и по-другому, например: