Дискретная математика

Раздел 1. Математическая логика

Тема 1. Логика высказываний

Тема 2. Булевы функции

Тема 3. Логика предикатов

Тема 4. Метод резолюций

Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F1,F2,...,Fk, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F1,F2,...,Fk тогда и только тогда, когда множество формул {F1,F2,...,Fk,ØG} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).

§1. Метод резолюций в логике высказываний

§2. Подстановка и унификация

§3. Метод резолюций для логики первого порядка

§4. Эрбрановский универсум множества дизъюнктов

§5. Семантические деревья, теорема Эрбрана

§6. Полнота метода резолюций в логике предикатов

§7. Стратегии метода резолюций

§8. Применение метода резолюций.

§9. Метод резолюций и логическое программирование

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


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


Логическая программа представляет собой совокупность формулы логики предикатов одного из следующих видов


(1) p(t1,...,tk).,

(2) q(s1,...,s1):-q1(s1,...,s1),...,qn(s1,...,s1).,


где P(t1,...,tk), q(s1,...,sl), q1(s1,...,sl),..., qn(s1,...,sl) – атомарные формулы логики первого порядка, буквы t и s с индексами – термы. Синтаксис языка логического программирования требует, чтобы в конце каждого выражения ставилась точка. Формулы первого вида называются фактами, а второго правилами. Формула q(s1,...,sl) называется заголовком правила (2). Выполнение программы тнтцтализируется запросом – формулой вида


(3) r1(u1,...,um),...,rn0(u1,...,um).,


где rj(u1,...,um) (1£j£n) – атомарные логики первого порядка, буквы u с индексами – термы.

Мы описали синтаксис основных конструкций логического программирования. Семантика обычно представляется в двух видах – логическая семантика и процедурная семантика.


Введем сначала логическую семантику. Каждому факту (1) поставим в соответствие формулу вида


(1/) F=("x*)p(t1,...,tk),


где кванторы общности навешаны на все переменные атомарной формулы (1). (Кроме переменных в термах могут быть, разумеется константы.) Правилу (2) аоставим в соответствие формулу вида


(2/) G=("x*)[q1(s1,...,sl) &...& qn(s1,...,sl)®q(s1,...,sl)],


где кванторы общности, как и выше, навешаны на все переменные. Запрос (3) получит в соответствие формулу


(3/) H=($x*)[r1(u1,...,um) &...& rn(u1,...,um)],


где квантор существования связывает все переменные. Пусть F1,...,Fa – формулы, соответствующие всем фактам, G1,...,Gb – всем правилам. Тогда значение пары (программа, запрос) в логической семантике есть утверждение о том, что формула H есть логическое следствие формул F1,...,,Fa, G1,...,Gb.


Операционная семантика – действия компьютера при ответе на запрос. Введем ее на примере следующей программы.


(1) r(a,b).,

(2) q(b,g(c)).,

(3) p(x,f(y)):–r(x,z), q(z,f(y)).,

(4) p(x,f(y)):–r(x,z) q(z,g(y)).,

(5) r(x,z):–q(f(x),g(z)).


(Здесь a,b,c,d – константы, x,y,z – переменные.) Номера в скобках не являются синтаксической конструкцией логического программирования, они проставлены для удобства ссылок.

Предположим, что запрос есть


(6) p(u,f(v)).


При вычислении ответа на этот запрос, интерпретатор формулирует цель r(u,f(v)) и пытается достичь ее, унифицируя цель с фактами. В нашем случае цель r(u,f(v)) не унифицируется ни с одним из фактов. Тогда интерпретатор пытается ее унифицировать с заголовком одного из правил. Это можно сделать с заголовком правила (4) с помощью подстановки s=(u=x,v=y). Запрос (6) принимает следующий вид


(6/) r(x,z),q(z,f(y))


и формируется цель r(x,z). Она достигается унификацией с первым фактом подстановкой s1=(x=a,z=b) и интерпретатор пытается достичь цели q(b,f(y)), но эта цель не унифицируется ни с одним из фактов, ни с заголовками правил. Следовательно цель q(b,f(y)) недостижима и происходит возврат к запросу (6/) и цели r(x,z). Делается попытка достичь этой цели при помощи правила (5), но эта попытка так же неудачна. Происходит возврат к запросу (6) и цели r(u,f(v)). (См. рис.4.9, где цели подчеркнуты.)


Рис. 4.9


Правило (3) «отработано». Интерпретатор унифицирует цель с заголовком правила (4) той же подстановкой s. Запрос принимает вид


(6//) r(x,z),q(z,g(y)),


а целью становится r(x,z). Цель унифицируется с первым фактом подстановкой s1 и ставится новая цель q(b,g(y)), которая унифицируется со вторым фактом подстановкой s2=(y=c). Исходная цель оказалась достижимой при результирующей подстановке s3=(u=a,v=c). Интерпретатор при этом может закончить работу и выдать подстановку s3. Возможен и другой режим работы интерпретатора, при котором он пытается найти все подстановки, ведущие к достижению цели.

Убедимся в том, что интерпретатор при поиске ответа на запрос фактически строит вывод с помощью правила резолюций.

Логическая семантика программе (1) – 5 ставит в соответствие следующие формулы:


F1=r(a,b),

F2=q(b,g(c)),

G1=("x,y,z)[r(x,z)&q(z,f(y))®p(x,f(y))],

G2=("x,y,z)[r(x,z)&q(z,g(y))®p(x,f(y))],

G3=("x,z)[q(f(x),g(z))®r(x,z)],

а запросу (6) – формулу


H=($u,v)p(u,f(v)).


Эта семантика, напомним, состоит в том, что H есть логическое следствие множества формул {F1,F2,G1,G2,G3}.

Как будет применяться в этой ситуации метод резолюций? Вначале будет составлено множество формул T={F1,F2,G1,G2,G3,ØH}. Затем каждая из формул множества T будет приведена к сколемовской нормальной форме, из которой будет получено множество дизъюнктов S. В нашем случае множество S состоит из дизъюнктов D1 – D6:


D1=r(a,b),

D2=q(b,g(c)),

D3=Ør(x,z)&Øq(z,f(g)Úp(x,f(y),

D4=Ør(x,z)ÚØq(z,g(y))Úp(x,f(y)),

D5==Øq(f(x),g(z))Úr(x,z),

D6=Øp(u,f(v)).


Отметим, что дизъюнкт D6 получился из формулы ØH.

Вывод пустого дизъюнкта будем осуществлять в соответствии с процедурной семантикой. Правило резолюций будет применяться так, что одним из исходных (для правила) дизъюнктов будет дизъюнкт D6 или его потомки. Попытка получить пустой дизъюнкт за один шаг, т.е. правило резолюций применить к паре {D1,D6} или {D2,D6}, не приводит к успеху. Применим тогда правило резолюций к паре {D3,D6}, получим резольвенту


D7=Ør(x,z)ÚØq(z,f(y))


с помощью подстановки s=(u=x,v=y). Попробуем теперь в D7 «уничтожить» литерал Ør(x,z). Это можно сделать с помощью дизъюнктов D1 и D5. Резольвентой дизъюнктов D1 и D7 будет дизъюнкт


D8=Øq(b,f(y)).


Единственный литерал, которого нельзя «уничтожить» ни одним из дизъюнктов D1 – D5. То же самое можно сказать и о резольвенте дизъюнктов D5 и D7.

Мы фактически доказали, что из множества дизъюнктов {D1,...,D5,D7} пустой дизъюнкт невыполним (см. пути в графе на рис. 4.9, приводящие к неудаче). Возьмем в таком случае резольвенту дизъюнктов D4 и D6:


D9=Ør(x,z)ÚØq(z,g(y)).


Литерал Ør(x,z) дизъюнкта D9 «уничтожили» с помощью D1 и подстановки s1=(x=a,z=b), получили дизъюнкт


D10=Øq(b,g(y)).


Резольвента дизъюнктов D2 и D10 дает пустой дизъюнкт, при этом используется подстановка s2=(y=c). Мы получили вывод пустого дизъюнкта из множества дизъюнктов {D1,...,D6} (см. путь в графе на рис. 4.9, приводящий к успеху).

Итак, интерпретатор при поиске ответа на запрос строит резолютивный вывод.

Задачи

Ответы, указания и решения

Раздел 2. Теория графов

Тема 5. Раскраски

Тема 6. Ориентированные графы и сети


Fair.ru Ярмарка сайтов
Rambler's Top100 Submitter.ru - Free promoting

Дизайн: Alex © 2002
Все вопросы и предложения можно направлять по адресу cad@mail.ustu.ru