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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Второй шаг. Проведем сколемизацию полученной формулы. Левее квантора существования стоит квантор всеобщности, значит, нужно заменить все вхождения переменной y новым унарным функциональным символом, зависящим от x. Получим формулу, находящуюся в сколемовской нормальной форме: Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов .

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

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

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

Подстановка — это множество вида {x1/t1,…, xn/tn}, где для всех i, xi — переменная, а ti — терм, причем Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов (отображение переменных в термы). При этом все переменные, входящие в подстановку, различны (для любого Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов ).

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

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

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

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

Пусть Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов и Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов — подстановки, Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов , Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов . Композиция Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов получается из множества Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов удалением пар Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов , где Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов и пар yi/si, где yi совпадает с одним из xj.

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

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

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

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

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

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

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

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

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

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

Шаг 1. Полагаем k=0, Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов .

Шаг 2. Если Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов — одноэлементное множество, останавливаем алгоритм, Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов — наиболее общий унификатор для S. В противном случае строим множество рассогласований Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов и переходим к третьему шагу.

Шаг 3. Если в Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов существуют переменная x и терм t такие, что x не входит в t, то полагаем что Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов . Увеличиваем на единицу k, переходим ко второму шагу. Иначе останавливаемалгоритм, множество S не унифицируемо.

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

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

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

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

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

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

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

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

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

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

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

Пример. Правило вывода modus ponens получается из правила резолюции, если взять в качестве родительских дизъюнктов C1=A, Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов . Контрарными литералами в применении этого правила будут A и Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов , резольвентой — формула B.

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

Пусть имеется два дизъюнкта C1 и C2, у которых нет общих переменных, L1 — литерал, входящий в дизъюнкт C1, L2 — литерал, входящий в дизъюнкт C2. Если литералы имеют наибольший общий унификатор Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов то дизъюнкт Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов называется резольвентой дизъюнктов C1 и C2. Литералы L1 и L2 называются контрарными литералами. То же правило записывается в графическом виде как

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

Здесь P1 и P2 — контрарные литералы, Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов — резольвента, полученная из дизъюнкта Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов применением унификатора Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов и Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов — родительские дизъюнкты, а Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов — наибольший общий унификатор P1 и P2.

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

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

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

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

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

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

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

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

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

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

B:–A1,A2,…,An.

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

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

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

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

Случайные записи:

Лекция 11: Интерпретация и полнота исчисления предикатов


Похожие статьи:

Добавьте постоянную ссылку в закладки. Вы можете следить за комментариями через RSS-ленту этой статьи.
Комментарии и трекбеки сейчас закрыты.