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

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

Пример.

1. – родительский дизъюнкт

и – контрарные литералы
- резольвента

2. – родительский дизъюнкт

и – контрарные литералы
- резольвента

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

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

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

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

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

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

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

Если дизъюнкт состоит только из отрицательных литералов, его называют вопросом.

Если дизъюнкт содержит и положительные и отрицательные литералы, то его называют правилом.

Правила вывода:

Prolog:

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

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

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

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

Основные понятия Пролога

Нормальная форма Бэкуса-Наура (БНФ), разработана в 1960 Джоном Бэкусом и Питером Науром и используется для формального описания синтаксиса языков программирования.

::= – "по определению" ("это", "есть"). Слева от разделителя располагается объясняемое понятие, справа - конструкция, разъясняющая его.

<>–для обозначения синтаксической конструкции

| – или

[] – необязательная конструкция

«-:» – если

«,» – и

«;» – или

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

1. Факты

2. Правила

Предложение имеет вид:

–заголовок, – тело.

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

Предикат в форме БНФ:

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

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

В Turbo Prolog предложения с одним и тем же предикатом в заголовке должны идти одно за другим. Такая совокупность предложений называется процедурой.

Правила - это предложения, истинность которого зависит от истинности одного или нескольких предложений. Обычно правила содержат несколько хвостовых целей, которые должны быть истинными для того, чтобы правило было истинным. В нотации БНФ правило будет иметь вид:

Примеры факта: мама("Наташа", "Даша").

Пример правила:

– переменные.

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

Свободная переменная – та, которая еще не получила значение. У неё нет никакого значения (ни ноль ни символ пробела). Второе название – неконкретизированная.

Переменная, которая получила какое-то значение и оказалась связанной с определённым объектом называетсясвязанной.

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

Исключение из правила определения правила области действия является анонимная переменная, которая обозначается «_». Каждая анонимная переменная - это отдельный объект.

Третьим специфическим видом предложений Пролога можно считать вопросы. Вопрос состоит только из тела и может быть выражен с помощью БНФ в следующем виде:

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

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

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

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

Вопрос:

мама(X,Даша).

Ответ:

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

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

Пример предиката, который будет находить максимум из двух чисел:

Второй способ:

В данной ситуации нам пригодится встроенный предикат «!», который называется cut (отсечение). Этот предикат предназначен для ограничения пространства поиска с целью повышения эффективности работы программ, он всегда завершается успешно. После того, как до него дошла очередь, он устанавливает «запор», который не даёт «откатится назад», чтобы выбрать альтернативные решения для уже «сработавших» подцелей, то есть для тех, которые расположены левее отсечения. На цели, расположенные правее отсечение не влияет. Кроме того, отсечение отбрасывает все предложения процедуры, расположенные после предложения, в котором расположено отсечение.

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

Примером красного отсечения имеется в реализации max2. Если убрать отсечение, предикат будет выдавать в качестве максимума 2 число, даже если оно меньше первого. Пример зелёного отсечения можно получить, если в запись с предикатом макс добавить отсечение. При их наличии предикат будет выдавать те же решения, что и без них.

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