Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов

Первый шаг. Приводим исходную формулу к предваренной нормаль­ной форме. Для этого:

1 пользуясь эквивалентностью А → В≡A⋁B исключим импликацию;

2 перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалент­ности:

(A⋁B)≡A⋀B

(A⋀B)≡A⋁B

(∃xA)≡∀xA

(∀xA)≡∃xA

А=А

3 переименовываем связанные переменные так, чтобы ни одна пе­ременная не входила в нашу формулу одновременно связанно и свободно.

4 выносим кванторы в начало формулы, используя эквивалентности:

QxA(x)⋁B≡Qx(A(x)⋁B), если B не содержит переменной x,a Q∊{∀,∃}

QxA(x) ⋀B≡Qx(A(x)⋀B), если B не содержит переменной x,a Q∊{∀,∃}

∀xA(x)⋀∀xB(x)≡∀x(A(x)⋀B(x))

∃xA(x)⋁∃xB(x)≡∃x(A(x)⋁B(x))

Q₁xA(x)⋁Q₂yB(y)≡ Q₁xQ₂y(A(x)⋁B(y)), где Q∊{∀,∃}

Q₁xA(x)⋀Q₂yB(y)≡ Q₁xQ₂y(A(x)⋀B(y)), где Q∊{∀,∃}

 

Второй шаг. Проведем сколемизацию, т.е. элиминируем в формуле квантор существования. Для этого для каждого квантора существования выполним следующий алгоритм.

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

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

Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме. Алгоритм ус­транения кванторов существования придумал Сколем в 1927 году.

Имеет место теорема о том. что формула и ее сколемизация эквива­лентны в смысле выполнимости.

 

Третий шаг. Элиминируем кванторы всеобщности. Полученная формула будет бескванторной и эквивалентной исходной в смысле вы­полнимости.

 

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

A⋁(В⋀С) = (A⋁B)⋀(A⋁C)

A⋀(В⋁С) = (A⋀B)⋁ (A⋀C)

 

Пятый шаг. Элиминируем конъюнкции, представляя формулу в ви­де множества дизъюнктов.

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

Теорема. Формула является тождественно ложной тогда и только тогда, когда множество дизъюнктов, полученных из неё, является невыполнимым

Напомним, что множество формул называется невыполнимым, если не существует такого означивания переменных, чтобы все формулы из этого множества были бы истинными.

Пример. Превратим формулу ∀x(P(x) → ∃y(P(y)⋁Q(x,y))) в эк­вивалентное ей множество дизъюнктов.

Первый шаг. Приведем исходную формулу к предваренной нормаль­ной форме. Элиминировав импликацию, получим формулу ∀x(P(x)⋁∃y(P(y)⋁Q(x,y))). Вынесем переменную у за скобки: ∀x∃y(P(x)⋁(P(y)⋁Q(x,y))). Это можно сделать, потому что форму­ла P(x) не зависит от переменной у. Если бы она зависела, то можно было бы переименовать связанную переменную у.

Второй шаг. Проведем сколемизацию полученной формулы. Левее квантора существования стоит квантор всеобщности, значит, нужно за­менить все вхождения переменной у новым унарным функциональным символом, зависящим от х. Получим формулу, находящуюся в сколемовской нормальной форме: ∀x(P(x)⋁(P(f(x))⋁Q(x,f(x)))).

Третий шаг. Элиминируем квантор всеобщности: P(x)⋁(P(f(x))⋁Q(x,f(x))).

В четвертом и пятом шагах необходимости нет, поскольку формула уже представляет собой дизъюнкт: P(x)⋁P(f(x))⋁Q(x,f(x)).

Следующая техника, лежащая в основе Пролога, с которой мы по­пробуем разобраться, — это унификация. Унификация позволяет отожде­ствлять формулы логики первого порядка путем замены свободных пере­менных на термы.

Подстановка — это множество вида {x₁/t_1,..., x_n/t_n}, где для всех i, x_i — переменная, а t_i — терм, причем х_i≠t_i (отображение переменных в термы). При этом все переменные, входящие в подстановку, различны (для любого i≠j х_i≠х_j).

Символом ε будем обозначать пустую подстановку.

Подстановка, в которой все термы основные, называется основной подстановкой.

Простое выражение — это терм или атомная формула.

Если А — простое выражение, а θ — подстановка, то Aθ получается путем одновременной замены всех вхождений каждой переменной из θ в А соответствующим термом. Аθ называется частным случаем (примером) выражения А. Содержательно подстановка заменяет каждое вхождение переменной х_i на терм t_i.

Пусть θ и η — подстановки. θ={x₁/t_1,...,x_n/t_n}, η ={y₁/s_1,...,y_n/s_n}. Композиция θη получается из множества {x₁/t₁η,...,x_n/t_nη, y₁/s₁,...,y_n/s_n}. удалением пар x_i/t_iη, где x_i=t_iη и пар y_i/s_i, где y_i совпадает с одним из x_j.

Пример. Пусть θ={x/f (у),y/z}, η={x/a,y/b,z/y}. Построим θη.

Для этого возьмем множество {x/f(b),y/y,x/a,y/b,z/y} и выбро­сим из него пары у/у (потому что заменяемая переменная совпадает с термом), х/а, у/b (потому что заменяемая переменная из подстановки η совпадает с заменяемой переменной из подстановки θ). Получим ответ: θη={x/f(b), z/y}.

Подстановка θ называется более обшей, чем подстановка η, если су­ществует такая подстановка γ, что η=θγ.

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

Пример. A=p(f(х),z) и В=р(у,а) унифицируемы. Можно взять в качестве их унификатора подстановку {y/f(x),z/a} или подстановку {y/f(a),x/a,z/a}.

Вообще говоря, две формулы могут иметь бесконечно много унифи­каторов. Унификатор q называют наиболее общим (или простейшим) унификатором простых выражений А и B, если он является более общей подстановкой, чем все другие унификаторы простых выражений А и В.

Пример. В рассмотренном выше примере наиболее общим унификатором является подстановка {y/f (a),z/a}.

Пусть S — конечное множество простых выражений. Определим множество d(S) разногласий (рассогласований). Зафиксируем самую левую позицию, на которой не во всех выражениях из S стоит один и тот же сим­вол. Занесем в d(S) подвыражения выражений из S, начинающиеся с этой позиции.

Пример. Пусть S=(p(f(х),h(y),а),р(f(х),z,a),p(f(х),h(y),b)}. Множество рассогласований для S d(S) = {h(y),z}.

 

Алгоритм унификации

 

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

Шаг 1. Полагаем k=0, δ₀=ε.

Шаг 2. Если S — одноэлементное множество, останавливаем алго­ритм: δ_k — наиболее общий унификатор для S. В противном случае стро­им множество рассогласований d(Sδ_k) и переходим к третьему шагу.

Шаг 3. Если в d(Sδ_k) существуют переменная x и терм t такие, что x не входит в t, то полагаем что δ_k+1=δ_k{x/t}. Увеличиваем на единицу k, пе­реходим ко второму шагу. Иначе останавливаем алгоритм, множество не унифицируемо.

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

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

Теперь можно перейти к рассмотрению метода резолюций.

В чем вообще заключается задача? Мы хотим построить алгоритм, который позволял бы нам автоматически давать ответ на вопрос, может ли быть выведено некоторое заключение из множества имеющихся по­сылок. Известно. что в общем случае даже для логики первого порядка такой алгоритм невозможен. Как правило, формальные системы, для которых можно построить подобный разрешающий алгоритм, обладают небольшой выразительной силой. К ним, например, относится логика высказываний и логика одноместных предикатов.

Однако Робинсон решил, что правила вывода, используемые компь­ютером при автоматическом выводе, не обязательно должны совпадать с правилами вывода, используемыми при «человеческом» выводе. В частно­сти, он предложил вместо правила вывода «modus ponens». которое утвер­ждает, что из А и А → В выводится В, использовать его обобщение, правило резолюции, которое сложнее понимается человеком, но эффективно реа­лизуется на компьютере. Давайте попробуем разобраться с этим правилом.

Правило резолюции для логики высказываний можно сформулиро­вать следующим образом.

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

Графически это правило можно изобразить так:

A⋁P, B⋁Р

A⋁B

Здесь A⋁P и B⋁Р — родительские дизъюнкты, Р и Р — контрар­ные литералы. A⋁B — резольвента.

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

Пример. Правило вывода «modus ponens» получается из правила ре­золюции, если взять в качестве родительских дизъюнктов C₁=A, C₂=A⋁B(≡А → В). Контрарными литералами в применении этого прави­ла будут A и нA, резольвентой — формула B.

Сформулируем правило резолюции для логики первого порядка.

Пусть имеется два дизъюнкта C₁ и C₂, у которых нет общих переменных, L₁ — литерал, входящий в дизъюнкт C₁, L₂ — литерал, входящий в дизъюнкт C₂ (C₁=A⋁L₁,C₂=B⋁L₂). Если литералы L₁ и L₂ имеют наибольший общий унификатор θ, то дизъюнкт ((C₁ -L₁)⋁(C₂ -L₂))θ называется резольвентой дизъюнктов C₁ и C₂. Литералы L₁ и L₂ называются контрарными литералами. То же правило записывается в графическом виде как

A⋁L₁, B⋁L ₂

(A⋁B)θ

Здесь L₁ и L₂ — контрарные литералы, (A⋁B)θ — резольвента, полу­ченная из дизъюнкта (A⋁B) применением унификатора θ. A⋁L₁ и B⋁L₂ — родительские дизъюнкты, а θ — наибольший общий унификатор L₁ и L₂.

Метод резолюций является обобщением метода «доказательства от противного». Вместо того чтобы пытаться вывести некоторую формулу-гипотезу из имеющегося непротиворечивого множества аксиом, мы доба­вляем отрицание нашей формулы к множеству аксиом и пытаемся выве­сти из него противоречие. Если нам удается это сделать, мы приходим к выводу (пользуясь законом исключенного третьего), что исходная формула была выводима из множества аксиом. Опишем более подробно.

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

Возможны, вообще говоря, три случая:

1. Этот процесс никогда не завершается.

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

3. На очередном шаге получена пустая резольвента. Это означает, что множество дизъюнктов невыполнимо и. следовательно, начальная формула выводима.

 

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

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

В сущности, метод резолюций несовершенен и приводит к «комби­наторному взрыву». Однако некоторые его разновидности (или страте­гии) довольно эффективны. Одной из самых удачных стратегий является линейная или SLD-резолюция для хорновских дизъюнктов (Linear resolution with Selection function for Definition clauses), то есть дизъюнктов, содержа­щих не более одного положительного литерала. Их называют предложени­ями или клозами.

Если дизъюнкт состоит только из одного положительного литерала, он называется фактом. Дизъюнкт, состоящий только из отрицательных литералов, называется вопросом (или целью или запросом). Если дизъюнкт содержит и позитивный, и негативные литералы, он называется прави­лом. Правило вывода выглядит примерно следующим образом А₁⋁A₂…⋁A_n⋁B. Это эквивалентно формуле А₁⋀A₂…⋀A_n→B, которая на Прологе записывается в виде

В:-А₁,A₂,…,A_n.

Логической программой называется конечное непустое множество хорновских дизъюнктов (фактов и правил).

При выполнении программы к множеству фактов и правил добавляется отрицание вопроса, после чего используется линейная резолюция. Ее специфика в том, что правило резолюции применяется не к произволь­ным дизъюнктам из программы. Берется самый левый литерал цели (под­цель) и первый унифицируемый с ним дизъюнкт. К ним применяется правило резолюции. Полученная резольвента добавляется в программу в качестве нового вопроса. И гак до тех пор. пока не будет получен пустой дизъюнкт, что будет означать успех, или до тех пор, пока очередную подцель будет невозможно унифицировать ни с одним дизъюнктом програм­мы, что будет означать неудачу.

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

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