Полнота метода резолюций означает что

Логические основы Пролога

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Источник

Полнота метода резолюций означает что

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

где X и Y — произвольные термы или целые дизъюнкты с любым набором термов, включая ноль; A и A — произвольные термы.

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

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

А, А → В ⇒ В или 0 ∨ А, А ∨ В, В ∨ 0 ⇒ 0.

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

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

Обращаем внимание на то, что посылка В здесь вообще не используется. Это необходимо иметь в виду: необязательно использовать все посылки (их число часто бывает избыточным) — главное получить ноль. Пусть дана клауза:

Доказательство ее справедливости следует начать с приведения ее в нормальную конъюнктивную форму:

Выпишем по порядку все посылки и далее начнем их склеивать (справа от дизъюнкта записаны номера используемых дизъюнктов):

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

5. В (1,4), 6. С (2,4), 7. В (3,6), 8. 0 (5,7).

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

Докажем одну и ту же клаузу двумя способами — в форме противоречия и форме тавтологии. Пусть дана клауза:

Доказательство в форме противоречия выглядит так:

Если по порядку пронумеровать четыре посылки, то ноль получается при следующих склейках:

5. В (1,2), 6. А ∨ С (1,6), 7. С (3,5), 8. 0 (4,7).

Доказательство в форме тавтологии выглядит аналогично:

5. В (1,2), 6. А ∧ С (1,6), 7. С (3,5), 8. 1 (4,7).

Метод резолюций легко поддается алгоритмизации. Это позволяет использовать его в логических языках программирования и, в частности, в ПРОЛОГЕ. Алгоритм склеек образует структуру древовидной формы (рис. 1.19) для следующей клаузы:

Источник

Вывод в логических моделях. Метод резолюций

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

Наиболее часто используются два метода. Первый – метод правил вывода или метод естественного (натурального) вывода, названный так потому, что используемый тип рассуждений в исчислении предикатов приближается к обычному человеческому рассуждению. Второй – метод резолюций. В его основе лежит исчисление резольвент.

В этой статье рассматривается второй метод. Метод резолюций предложен в 1930г. в докторской диссертации Эрбрана для доказательства теорем в формальных системах первого порядка.

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

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

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

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

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

В методе резолюций множество предложений обычно рассматривается как составной предикат, содержащий несколько предикатов, соединенных логическими функциями и кванторами существования и общности. Так как одинаковые по смыслу предикаты могут иметь разный вид, то предложения преобразуются в клаузальную форму – разновидность конъюнктивной нормальной формы (КНФ), в которой удалены кванторы существования, всеобщности, символы импликации, равнозначности и др. Клаузальную форму называют сколемовской конъюнктивной формой.

В клаузальной форме вся исходная логическая формула представляется в виде множества предложений (клауз) , называемых клаузальным множеством :

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

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

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

Если содержит пустое предложение , то противоречиво (невыполнимо). Если предложение не является пустым, то делается попытка вывода предложений пока не будет получено пустое (что всегда будет иметь место для невыполнимого ).

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

Предложение , вновь сформированное из имеющихся и , называется резольвентой и . Например:

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

доказывает истинность выдвинутого предположения:

Поскольку в логике предикатов в предложениях допускается наличие переменных, то для нахождения контрарных пар требуется введение операции унификации (подстановки константы вместо переменной в предикаты, имеющие одинаковые предикатные символы, но разные литеры). Алгоритм унификации разработали в 1966 г. Ж. Питра и независимо от него – Дж. Робинсон: чтобы унифицировать два различных выражения, отыскивается наиболее общий унификатор – НОУ (подстановка, при которой выражение с большей описательной мощностью согласуется с выражением, имеющим малую описательную мощность). Наличие этого алгоритма позволило реализовать метод резолюций Эрбрана в виде программы для ЭВМ.

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

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

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

Пример: вывод решения в логической модели на основе метода резолюций.

Даны утверждения:

Требуется методом резолюций доказать утверждение «Сократ смертен».

Решение:

Шаг 1. Преобразуем высказывания в дизъюнктивную форму:

Шаг 2. Запишем отрицание целевого выражения (требуемого вывода), т.е. «Сократ бессмертен»:

Шаг 3. Cоставим конъюнкцию всех дизъюнктов (т. е. построим КНФ), включив в нее отрицание целевого выражения:

Шаг 4. В цикле проведем операцию поиска резольвент над каждой парой дизъюнктов:

Получение пустого дизъюнкта означает, что высказывание «Сократ бессмертен» ложно, значит истинно высказывание «Сократ смертен».

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

Источник

Электронная библиотека

Пусть А₁, …, А_m, В – формулы. Рассмотрим доказательство секвенции А₁, …, А_m ® В.

Определение 2: Формула, в которой символом Ú объединены более одного литерала, называется предложением.

Порядок преобразования в клаузальную форму

1) Ограничение свободных переменных

2) Переименование переменных

3) Удаление символа É

Часть формулы В É С заменим на ØВ Ú С.

f – вновь выбранный функциональный n – местный символ.

При n = 0 он заменяется на вновь выбранную константу, которая до сих пор не применялась. Все это – сколемовская функция и сколемовская постоянная.

f-g – сколемовские функции

a – сколемовская постоянная, f — функция

6) Перемещение » вперед

Часть «х перемещается в префиксную часть программы.

7) Перемещение Ú относительно Ù

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

Унификация и правила вывода

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

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

Однако для этой задачи существует более рациональный путь отыскания пустого множества:

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

Пусть дана клауза: A, A ® B, B ® (A ® C) |—

Запишем исходную клаузу в форме противоречия:

Теперь сделаем это в форме тавтологии:

На основе этой таблицы можно установить следующие справедливые отно-шения:

Источник