Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

11.7. МЕТОД РЕЗОЛЮЦИЙ

321

§ 11.7. МЕТОД РЕЗОЛЮЦИЙ И ЕГО СРАВНЕНИЕ

С МЕТОДОМ ЕСТЕСТВЕННОГО ВЫВОДА

И семантические таблицы, и естественный вывод были неудобны для

реализации на примитивных вычислительных машинах 60-х гг. Ситу-

ация еще осложнялась тем, что их качественная реализация требовала

сложных структур данных и методики не ниже по уровню, чем совре-

менное объектно-ориентированное программирование, а этих средств в

те времена еще не было. Поэтому был изобретен метод, идеально под-

ходивший для реализации на достаточно примитивных вычислитель-

ных системах и завоевавший практически монопольное положение за

последние десятилетия

. Разберем сам метод, его достоинства и недо-

статки.

Метод резолюций базируется на приведении формул классической

логики к стандартной форме. Тавтологии, используемые при этом при-

ведении, не сохраняются в неклассических логиках, и поэтому в прин-

ципе метод резолюций с самого начала создавался (в отличие от се-

мантических таблиц и естественного вывода) как ориентированный на

классическую логику. Такая специализация явилась одной из предпосы-

лок его достаточно высокой эффективности для ряда задач и, соответ-

ственно, его успеха.

Приведение формулы к виду, пригодному для применения метода

резолюций, производится в несколько этапов. Первый — вынос всех

кванторов вперед. При этом пользуются следующими эквивалентностя-

В науке, так же как и в биологических сообществах, существует эффект экологиче-

ской ниши. Если есть потребности, не удовлетворяемые ни одной из существующих

распространенных систем, то первая из систем, удовлетворившая их, становится клас-

сической и, независимо от своих достоинств и недостатков, очень трудно вытесняемой.

Конкурент обязан здесь не просто быть на порядок лучше, но еще и суметь провести

рекламную кампанию. Более того, те, кто уже привык к классической системе, как пра-

вило, просто не желают знать ничего нового, так что надеяться здесь можно лишь на

новое поколение. Рассматриваемый метод резолюций завоевал именно такое положе-

ние.

322

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

ми классической логики:

∀x A(x) & B ⇔ ∀x(A(x) & B) ∃x A(x) & B ⇔ ∃x(A(x) & B)

∀x A(x) ∨ B ⇔ ∀x(A(x) ∨ B) ∃x A(x) ∨ B ⇔ ∃x(A(x) ∨ B)

(∀x A(x) ⇒ B) ⇔ ∃x(A(x) ⇒ B) (B ⇒ ∀x A(x)) ⇔ ∀x(B ⇒ A(x))

(∃x A(x) ⇒ B) ⇔ ∀x(A(x) ⇒ B) (B ⇒ ∃x A(x)) ⇔ ∃x(B ⇒ A(x))

∀x A(x) ⇔ ∃x

A(x)

∃x A(x) ⇔ ∀x

A(x)

(11.4)

Заметим, что эти правила точно так же могут использоваться и нао-

борот, для вноса кванторов внутрь формулы. Поэтому появляются две

стандартные формы в классической логике: предваренная, где кванторы

вынесены наружу, и водворенная, где они внесены внутрь. Рассмотрим

пример.

∀x(∃y(∀z B(z) ⇒ ∀u D(u, y)) ∨ ∃v(∀w E(v, w) & ∀q H(x, q))). (11.5)

Предваренной формой этой формулы будет, в частности,

∀x ∃y ∃z ∀u ∃v ∀w ∀q((B(z) ⇒ D(u, y)) ∨ (E(v, w) & H(x, q))),

(11.6)

а также,скажем (при другом порядке выноса независимых друг от друга

кванторов),

∀x ∃v ∀q ∀w ∃y ∀u ∃z((B(z) ⇒ D(u, y)) ∨ (E(v, w) & H(x, q))).

(11.7)

Водворенной формой будет, в частности,

(∀z B(z) ⇒ ∃y ∀u D(u, y)) ∨ ∀x ∃v(∀w E(v, w) & ∀q H(x, q)). (11.8)

Здесь квантор по

x не перенесен еще глубже внутрь потому, что ∃ и ∀

неперестановочны. Теперь можно дать и определение.

Определение 11.7.1.

Формула находится в

предваренной

форме, если

она имеет вид

K~x A(~x)

, где

— последовательность кванторов,

кван-

торов не содержит.

Формула находится в

водворенной

форме, если область действия ни

одного квантора не может быть уменьшена применением эквивалентно-

стей (11.4).

Как уже отмечалось, водворенная форма лучше с точки зрения по-

нимания и обратного перевода на естественный язык. Предваренная не-

сколько удобней для доказательства некоторых математических резуль-

татов.

11.7. МЕТОД РЕЗОЛЮЦИЙ

323

Рассмотрим один из этих результатов, послуживший идейной осно-

вой метода резолюций. Интуитивно сочетание кванторов ∀x ∃y может

пониматься как утверждение о существовании функции, строящей y по

x. Точные выражения этого интуитивного принципа бывают различны-

ми (одним из них является аксиома выбора.) Молодой французский ма-

тематик Ж. Эрбран

в 1930 г. доказал теорему, которая может считать-

ся алгоритмическим уточнением этого интуитивного соответствия для

случая классической логики. А именно, рассмотрим предваренную фор-

мулу

K~x A(~x). (11.9)

Переменные, связанные кванторами всеобщности, обозначим через x

а кванторами существования — через y

.Сопоставим каждому квантору

∃y

функцию f

, . . . , x

), зависящую от всех переменных в стоящих

ранее кванторах всеобщности (нульместная функция в данном случае

отображается как константа). Тогда наша формула преобразуется к виду

∀x

. . . ∀x

A(~x,

f(~x)). (11.10)

Такое преобразование называется сколемизацией, а сами функции —

сколемовскими функциями

. Теперь возьмем константу c

, если у нас

вообще не было нульместных функций, и построим универс из термов,

образующихся применением сколемовских функций к имеющимся у нас

константам. Этот универс ввел в рассмотрение Эрбран, и поэтому его

называют эрбрановским универсом.

Теорема 11.3. (Теорема Эрбрана, первая форма)Формула (11.9) явля-

ется противоречием тогда и только тогда, когда найдутся такие си-

стемы термов из эрбрановского универса

, . . . ,

, что конъюнкция

частных примеров формулы (11.10)

)) & ∙∙∙ & A(

)) (11.11)

Как часто было в логике, история данного открытия была несколько трагичной. Эр-

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

данная теорема. Но данное им доказательство было длинным и непонятным. Уже в 50-х

гг. появились другие доказательства, а в начале 60-х в диссертации Эрбрана была най-

дена ошибка. Заметим, что саму теорему никто под сомнение не брал, но пользоваться

ею стали лишь после появления понятных доказательств. А Эрбран вскоре после защи-

ты диссертации трагически погиб и не успел изведать позора либо поправить ошибку

сам...

Поскольку впервые такие функции для замены кванторов стал систематически ис-

пользовать Т. Сколем.

324

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

является противоречием в исчислении высказываний.

Доказательство. Строим семантическую таблицу формулы

|=(11.9).

Движением по дереву секвенций от корня к листьям сопоставим каждой

встретившейся в ней вспомогательной константе терм эрбрановского

универса. А именно, константе, ‘взятой из воздуха’, сопоставим c

. Кон-

стантам, получившимся в результате снятия начальных кванторов су-

ществования, сопоставим соответствующие сколемовские константы.

Если константа c

получилась из внутреннего квантора существования,

то предшествующие x

, . . . , x

были заменены на ранее построенные

константы, которым по построению уже сопоставлены термы r

, . . . , r

Тогда сопоставляем c

терм f

, . . . , r

Теперь прослеживаем все подстановки вместо ~x, произведенные в

процессе построения таблицы, и каждая из них дает нам одну из систем

термов. Первыми шагами построения таблицы для |=(11.11) являются

порождения всех |= A(

)), а затем воспроизводим все шаги исход-

ной таблицы, кроме снятия кванторов.

Как и обычно, для применений теоремы нужно проварьировать ее

формулировку.Поэтому рассмотрим вторую формулировку теоремы Эр-

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

Инвертируем процесс сколемизации, теперь на переменные будем заме-

нять кванторы существования, а на функции — кванторы всеобщности.

Полученная форма будет иметь вид

∃y

. . . ∀y

A(~g(~y), ~y). (11.12)

При инверсной сколемизации точно так же появляется эрбрановский

универс и имеет место следующая

Теорема 11.4. (Теорема Эрбрана, вторая форма)Формула (11.9) явля-

ется тавтологией тогда и только тогда, когда найдутся такие си-

стемы термов из эрбрановского универса

, . . . ,

, что дизъюнкция

частных примеров формулы (11.12)

) ∨ ∙∙∙ ∨ A(

) (11.13)

является тавтологией в исчислении высказываний.

Доказательство данной теоремы аналогично предыдущей. Именно

вторая форма теоремы Эрбрана была использована создателем метода

резолюций Дж. Робинсон для разработки машинного алгоритма.

11.7. МЕТОД РЕЗОЛЮЦИЙ

325

Но предварительно был проделан еще один шаг в приведении фор-

мул к стандартному виду. В исчислении высказываний еще с XIX века

известны две стандартные формы для исчисления высказываний: конъ-

юнктивная и дизъюнктивная. Конъюнктивная форма получается из та-

блиц истинности. Каждое значение логических переменных

, при ко-

тором формула

A истинна, представляется как конъюнкция атомарных

формул или атомов: элементарных формул либо их отрицаний. Такие

конъюнкции называются конъюнктами.Конъюнкты дизъюнктивно объ-

единяются и получается формула, эквивалентная A. Отрицанием конъ-

юнктивной нормальной формы для

получается дизъюнктивная нор-

мальная форма для A, в которой атомарные формулы соединяются дизъ-

юнкциями, а получившиеся дизъюнкты — конъюнкциями.

При работе методом резолюций, так же, как и в семантических та-

блицах, начинают с отрицания формулы. Поэтому используется альтер-

нативная сколемизация, а пропозициональная часть формулы предста-

вляется как конъюнктивная нормальная форма, а затем отрицается и

превращается в конъюнкцию дизъюнктов.

Самым блестящим достижением Дж. Робинсон и метода резолюций

явилась формулировка крупноблочного правила, соединяющего в себе

обобщенную подстановку и шаг логического вывода. Это правило и бы-

ло названо правилом резолюции.

Дадим критерий, когда две последовательности термов с одинако-

вым числом членов могут быть приведены к одинаковому виду подста-

новкой вместо свободных переменных.

Определение 11.7.2. Подстановка

—множество пар вида

(x, t)

,где

—

переменная,

— терм, причем все первые члены в этих парах различ-

ны

. Применение подстановки

к терму

обозначается

tσ

и определят-

ся индуктивно, так же, как в определении подстановки для выражений.

xσ = t

, если

(x, t) ∈ σ

xσ = x

, если нет пары

(x, t) ∈ σ

cσ = c

— константа.

f(t

, . . . , t

)σ = f(t

σ, . . . , t

σ).

Можно было бы сказать, что подстановка — частичная функция из переменных в

термы, но мы уже сталкивались и еще столкнемся с коварством различных смыслов

таких понятий. Поэтому сформулируем чуть длиннее и скучнее, но однозначно.

326

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

Композиция подстановок

σ, $

определяется следующим образом:

σ$ = {(x, $t) | (x, t) ∈ σ}.

σ ≥ ϑ ⇔ ∃$ ϑ = σ$

(читается:

накрывает

). Если каждая из двух

подстановок накрывается другой, то они эквивалентны. Подстановка

унифицирует последовательности термов

, . . . , t

, . . . , r

, если

для всех

i t

σ = r

σ.

Легко доказать, что отношение эквивалентности подстановок дей-

ствительно является эквивалентностью и что отношение накрытия —

предпорядок, согласованный с нею.

Теорема 11.5. (Теорема об унификации) Для каждых двух унифициру-

емых последовательностей термов существует унифицирующая под-

становка, накрывающая любую другую такую подстановку.

Доказательство. Проведем построение, которое за конечное число ша-

гов даст такую подстановку

σ либо выяснит, что ее нет.

Шаг 0.

Вначале положим подстановку пустым множеством.

Шаг 1.

Ищем в последовательностях пару термов, каждый из которых

начинается с функционального символа. Если соответствующие функ-

циональные символы различны, то две последовательности неуни-

фицируемы, если же они совпадают, заменяем члены f(s

, . . . , s

)

и g(q

, . . . , q

) на последовательности s

, ..., s

и q

, ..., q

, соответ-

ственно.

После этого шага во всех парах соответствующих друг другу термов

хотя бы один член является переменной либо константой.

Шаг 2.

Удаляем из последовательностей все одинаковые члены, нахо-

дящиеся на одинаковых местах. Если после этого хотя бы в одном ме-

сте встретятся две соответствующие друг другу (различные) константы,

унификация невозможна.

Теперь в каждой из пар термов хотя бы один является переменной.

Шаг 3.

Если первой парой является пара (x, t), то если t содержит x,

заключаем, что унификация невозможна, а если t не содержит x, то до-

бавляем к σ пару (x, t), выбрасываем первые члены из двух последова-

тельностей и заменяем остальные r на r{(x, t)}. Если после этого по-

явились пары, оба компонента которых не являются переменными, то

возвращаемся к шагу 1. Симметрично действуем в случае, когда пере-

менной является второй компонент пары.

11.7. МЕТОД РЕЗОЛЮЦИЙ

327

Шаг 4.

Если длина обеих последовательностей дошла до 0, унифициру-

ющая подстановка найдена.

Данный алгоритм всегда кончает работу, потому что в любом цикле

количество переменных уменьшается хотя бы на 1. То, что построенная

унификация накрывает все остальные, легко показать индукцией по по-

строению

Унифицирующая подстановка, накрывающая все остальные, назы-

вается наиболее общим унификатором.

Правило резолюции состоит в том, что для двух дизъюнктов вида

P (

t) ∨ Q

P (~r) ∨ R

ищется подстановка σ, унифицирующая

и ~r. Если она находится, то в

результате применения правила получается дизъюнкт (Q ∨ R)σ.

Еще одной красивой находкой в методе резолюций явилось предста-

вление дизъюнктов как множеств атомов. Поскольку в множестве поря-

док элементов не играет роли и не может быть дублируемых, многие

тонкие, но неприятные вопросы сами собой отпали.

Поскольку в методе резолюций рассуждают от противного, форму-

ла считается доказанной, если в результате последовательности резо-

люций получается ложь, представлением которой служит пустой дизъ-

юнкт.

На примерах из метода резолюций мы долго останавливаться не бу-

дем, поскольку они изложены в множестве учебников и достаточно про-

сто написанных монографий. Мы сошлемся лишь на классический, ак-

куратно и просто написанный труд [32]. Здесь мы даем лишь необходи-

мый материал для решения нескольких упражнений и первичного овла-

дения данным методом.

Пример 11.7.1.

(Чень, Ли)

Некоторые пациенты любят своих докторов.

Ни один пациент не любит знахаря. Значит, ни один доктор — не зна-

харь.

Решение (этих же авторов).

Переведем посылки и заключения на

формальный язык:

⇔ ∃x(P (x) & ∀y(D(y) ⇒ L(x, y))),

⇔ ∀x(P (x) ⇒ ∀y(Q(y) ⇒

L(x, y))),

G ⇔ ∀x(D(x) ⇒

Q(x)).

328

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

Поскольку проверяемое утверждение имеет вид

& F

⇒ G

, после

отрицания оно переходит в

& F

. При приведении к предва-

ренной форме ни один квантор

∃

не попадает после

∀

, так что ни одной

сколемовской функции не появляется. В итоге мы получаем следующие

дизъюнкты:

(1) P (a)

(2)

D(y) ∨ L(a, y)



из

(3)

P (x) ∨

Q(y) ∨

L(x, y)

из

(4) D(b)

(5) Q(b)



из

Методом резолюций получается следующий вывод пустого дизъюнкта:

(6) L(a, b)

резольвента (4) и (2)

(7)

Q(y) ∨

L(a, y)

резольвента (3) и (1)

(8)

L(a, b)

резольвента (7) и (5)

(9) 

резольвента (6) и (8)

Конец решения.

Упражнения к § 11.7

11.7.1. Найдите ошибку в решении примера 11.7.1

§ 11.8. ОКОЛЬНЫЕ ПУТИ

КАК СРЕДСТВО СОКРАЩЕНИЯ ВЫВОДА

Мы рассмотрим теперь вопрос о недостатках метода резолюций, кото-

рые он, обладая огромными достоинствами, обязан иметь. Одним из не-

достатков является необходимость предварительного приведения фор-

мул к стандартной форме, после чего содержательный смысл порою те-

ряется, а длина формул может резко возрасти. Он неразрывно связан

с другим, неустранимым недостатком. Именно из-за этого недостатка,

глубоко спрятанного и в методе резолюций, и в методе семантических

таблиц,математическое доказательство оказалось ближе всего по струк-

туре к естественному выводу.

Для нахождения этой ошибки не обязательно разбираться в методе резолюций.

11.8. ОКОЛЬНЫЕ ПУТИ КАК СРЕДСТВО СОКРАЩЕНИЯ ВЫВОДА

329

Покажем, что естественный вывод может быть невообразимо коро-

че резолюционного. Мы базируемся здесь на примере петербургского

логика В. П. Оревкова, приведенном, в частности, в дополнении к пере-

воду книги [32]. Его идея следующая. Сформулировать несколько пред-

ложений таким образом, чтобы, во-первых, их можно было бы проин-

терпретировать на множестве натуральных чисел, во-вторых, после ско-

лемизации единственной доступной функцией оказалась бы

Sx = λx x + 1,

и, в-третьих, нам удалось бы доказать существование числа

= 2

...

(n раз).

Для этого достаточно определить “всего лишь” x

при помощи предика-

та P (x, y, z), истинного, когда x

= z. А наши a

можно было бы затем

определить при помощи последовательности кванторов существования

∃x

. . . x

(P (2, 0, x

) & ∙∙∙ & P (2, x

n−1

, x

)). (11.14)

Умножением и сложением натуральных чисел здесь не воспользуешь-

ся, поскольку описывающие их формулы дадут соответствующие ско-

лемовские функции, но можно пройти окольным путем. Воспользуемся

тем, что функция

ϕ(x, y) = x + 2

определяется системой рекурсивных уравнений



ϕ(x, 0) = x + 1

ϕ(x, y + 1) = ϕ(ϕ(x, y), y)

(11.15)

и распишем их на языке логики предикатов:

∀w ∃v P (w, 0, v) &

∀uvw(∃y(P (y, 0, u) & ∃z(P (v, y, z) & P (z, y, w)))

⇒ P (v, u, w)).

(11.16)

Для того чтобы определить формулу, выражающую существование

введем сокращения:

, x)

= ∃v

P (b

, x, v

)

∙∙∙

i+1

, x)

= ∃v

i+1

(P (b

, x, v

i+1

) & B

, v

i+1

)).

330

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

При предобработке для метода резолюций формулы (11.16) ⇒ B

(0, 0)

получаются следующие дизъюнкты:

P (x, 0, s(x))

P (y, 0, u) ∨

P (v, y, z) ∨

P (z, y, w) ∨ P (v, u, w)

P (0, 0, v

) ∨

P (0, v

, v

k−1

) ∨ ∙∙∙ ∨

P (0, v

, v

(11.17)

При каждой унификации единственная имеющаяся функция

s итериру-

ется не более одного раза.

Чтобы коротко доказать ∀b

∀x B

(x), исходя из (11.16), восполь-

зуемся следующим приемом. Дадим серию индуктивных определений,

каждое из которых содержательно будет означать одно и то же — нату-

ральный ряд, но шаг каждого последующего будет равен многим шагам

предыдущего.

∗

(x, y)

= ∃v

P (x, y, v

∙∙∙

∗

i+1

= ∃v

i+1

) & P (x, y, v

i+1

)),

(x)

= ∀w

∃v

P (w

, x, v

∙∙∙

i+1

(x)

= ∀w

i+1

) ⇒ A

∗

i+1

, x)).

(11.18)

Содержательно каждое

можно интерпретировать как индукцию по

определению для предиката ∀w

∃v

P (w

, x, v

) и определения нату-

рального ряда прыжками через

...

(n раз) членов. Каждое A

i+1

выво-

дится из A

, а из последнего из них элементарно выводится B

Но логическая сложность формул A

быстро возрастает с увеличе-

нием номера. Если же разрешить использовать окольные пути лишь по

формулам ограниченной сложности, то длина вывода B

начинает су-

перэкспоненциально возрастать, как только исчерпается потенциал воз-

можных определений. Поэтому ни метод резолюции, ни метод семанти-

ческих таблиц не может даже в принципе состязаться с естественным

выводом при доказательстве трудных формул

Правда, большинство практически нужных формул вполне пригодны для примене-

ния методов без окольных путей. Но как и везде, неприятность может поджидать в

самый неожиданный момент для внешне безобидных утверждений. Одним из таких

утверждений является теорема Кантора-Шредера-Бернштейна 5.2.