Метод резолюций

 

Логическое программирование является, пожалуй, наиболее впечатляющим примером применения идей и методов математической логики (точнее, одного из ее разделов - теории логического вывода) в программировании.

Идея использования языка логики предикатов первого порядка в качестве языка программирования возникла еще в 60-ые годы, когда создавались многочисленные системы автоматического доказательства теорем и основанные на них вопросно-ответные системы. Суть этой идеи заключается в том, чтобы программист не указывал машине последовательность шагов, ведущих к решению задачи, как это делается во всех процедурных языках программирования, а описывал на логическом языке свойства интересующей его области, иначе говоря, описывал мир своей задачи. Другие свойства и удовлетворяющие им объекты машина находила бы сама путем построения логического вывода.

Первые компьютерные реализации систем автоматического доказательства теорем появились в конце 50-х годов, а в 1965г. Робинсон предложил свой метод резолюций, который и по сей день лежит в основе большинства систем поиска логического вывода.

Робинсон пришел к заключению, что правила вывода, которые следует применять при автоматизации процесса доказательства с помощью компьютера, не обязательно должны совпадать с правилами вывода, используемыми человеком. Он обнаружил, что общепринятые правила вывода, например, правило modus ponens, специально сделаны “слабыми”, чтобы человек мог интуитивно проследить за каждым шагом процедуры доказательства. Правило резолюции более сильное, оно трудно поддается восприятию человеком, но эффективно реализуется на компьютере.

Вскоре метод резолюций был использован в качестве основы нового языка программирования. Так в 1972 году родился язык Пролог (“ПРОграммирование в терминах ЛОГики”), быстро завоевавший популярность во всем мире.

Сформулируем сначала правило резолюций в рамках исчисления высказываний. Пусть A, B и X - формулы. Предположим, что две формулы AÚX и BÚØX - истинны. Если X тоже истина, то отсюда можно заключить, что B истинна. Наоборот, если X ложна, то можно заключить, что A истинна. В обоих случаях формула AÚB истина. Это логическое следствие мы можем записать в виде правила

AÚX, BÚØX |= AÚB,

которое можно записать также в виде

ØXÉA, XÉB |= AÚB.

В том частном случае, когда X - высказывание, а A и B - элементарные дизъюнкции, то это правило называется правилом резолюций. Сравним это правило с уже известными нам:

цепное правило: ØA É X, X É B |= ØA É B,

модус поненс: X, XÉB |= B.

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

Доказательства, основанные на принципе резолюций, выделяются среди прочих тем, что они дают возможность использовать средства автоматического доказательства, применяемые в логическом программировании.

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

1. Приводим все посылки и отрицание заключения, принятое в качестве дополнительной посылки, к конъюнктивной нормальной форме:

а) устраняем символы É и ~ с помощью эквивалентностей

A~B = (AÉB)& (BÉA),

AÉB = ØAÚB;

б) продвигаем отрицания внутрь с помощью закона де Моргана;

в) применяем дистрибутивность AÚ (B&C) = (AÚB)& (AÚC).

2. Теперь каждая посылка превратилась в конъюнкцию элементарных дизъюнктов (будем их в дальнейшем называть просто дизъюнктами), может быть, одночленную. Выписываем каждый дизъюнкт с новой строки; все дизъюнкты истинны, так как конъюнкция истинна по предположению.

3. Каждый дизъюнкт - это дизъюнкция (возможно, одночленная), состоящая из переменных и отрицаний переменных. Именно к ним применим метод резолюций. Берем любые два дизъюнкта, содержащие одну и ту же переменную, но с противоположными знаками, например,

XÚYÚZÚØP,

XÚPÚW.

Применяем правило резолюции и получаем XÚYÚZÚW.

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

В качестве примера рассмотрим доказательство соотношения

PÚQ,PÉR,QÉS |= RÚS.

Приводим посылки к нормальной форме и выписываем их на отдельных строках.

 

PÚQ	(1)
ØPÚR	(2)
ØQÚS	(3)

 

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

Ø(RÚS) º ØR&ØS

 

ØR	(4)
ØS	(5)

 

Выводим пустой дизъюнкт с помощью резолюции.

 

ØP из (2) и (4)	(6)
Q из (1) и (6)	(7)
ØQ из (3) и (5)	(8)
пустой из (7) и (8)

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

Точнее, пусть нам дано множество функциональных символов f₁, f₂, f₃,..., каждый функциональный символ имеет вполне определенную местность, т.е. требует определенное количество аргументов.

Множество термов - это наименьшее подмножество языка логики предикатов, удовлетворяющее двум условиям:

а) переменные и константы суть (атомарные) термы;

в) если f_i - функциональный символ местности r, а t₁, t₂, ..., t_r - термы, то f_i(t₁, t₂, ..., t_r) - терм.

Мы будем называть формулу атомарной, если она выражается каким-то n-местным предикатом, аргументами которого служат термы. Используя атомарные формулы как первоначальные, понятие формулы общего вида определяем как в 4.1.

Фразовая форма логики предикатов - это способ записи формул, при котором употребляются только связки &, Ú и Ø. Литерал - это позитивная или негативная атомарная формула. Каждая фраза (или клауза) - это множество литералов, соединенных символом Ú. Фразу можно рассматривать как обобщение понятия импликации. Если A и B - атомарные формулы, то формула

AÉB
может также быть записана как

B Ú ØA.
Простейшая фраза содержит только один литерал, позитивный или негативный.

Фраза с одним позитивным литералом называется фразой (или клаузой) Хорна. Любая фраза Хорна представляет импликацию: так, например,

D Ú ØF Ú ØE равносильно (F&E) É D.

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

P(a) Ú ØQ(b,d),	(1)
Q(b,d) Ú ØR(b,d).	(2)

Поскольку во фразе (1) содержится негативный литерал ØQ(b,d), а во фразе (2) - соответствующий позитивный литерал Q(b,d) и аргументы обоих литералов могут быть унифицированы (т.е. b унифицируется с b, а d унифицируется с d), то фраза (1) может быть резольвирована с фразой (2). В результате этого получается фраза (3), которая называется резольвентой:

P(a) Ú ØR(b,d).

(3)

Фразы (4) и (5) не резольвируются друг с другом, так как аргументы литералов Q не поддаются унификации:

P(a) Ú ØQ(b,d),	(4)
Q(d,d) Ú ØR(b,d).	(5)

Унификация переменных. Во фразовой форме не употребляется явная квантификация переменных. Неявно, однако, все переменные квантифицированы кванторами всеобщности. Так, во фразе Q(x,y)ÚØR(x,y) подразумевается наличие кванторов:

"x"y (Q(x,y)ÚØR(x,y)).

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

P(a) Ú ØQ(a,b),	(6)
Q(x,y) Ú R(x,y)	(7)

резольвируемы, поскольку аргументы литерала Q унифицируются. При этом переменная x унифицируется с константой a, а переменная y - с константой b. Обратите внимание, что во фразе (8), т.е. в резоль­венте

P(a) Ú ØR(a,b),

(8)

переменные, служившие аргументами R во фразе (7), теперь заменены константами.

 

Следующий рекурсивный алгоритм выясняет унифицируемы ли два терма S и T.

1. Если S и T - константы, то S и T - унифицируемы т. и т. т., когда они являются одним и тем же объектом.

2. Если S - переменная, а T - произвольный терм, то они унифицируемы и S приписывается значение T. Наоборот, если T - переменная, а S - произвольный терм, то T получает в качестве значения S.

3. Если S и T - не атомарные термы, то они унифицируемы т. и т. т., когда а) S и T имеют одинаковый главный функциональный символ и б) все их соответствующие компоненты (подтермы) унифицируемы.

Результирующая конкретизация определяется унификацией компонент.