Мы обычно пользуемся языком для того, чтобы делать утверждения, касающиеся интересующей нас области. Отношения между языком и описываемой им областью определяется семантикой этого языка. Правильно построенные формулы исчисления предикатов как раз являются теми выражениями, которые мы будем использовать в качестве утверждений, касающихся интересующей нас области. Говорят, что правильно построенные формулы принимают значения T или F в зависимости от того, являются эти утверждения в этой области истинными или ложными. Приемы обращения с правильно построенными формулами позволяют строить умозаключения, относящиеся к некоторой области, и, следовательно, могут представить интерес при создании принятия решения, требующего такого умозаключения.[2]

1.3.1 Унификация и принцип резольвенции в исчислении

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

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

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

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

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

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

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

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

Принцип резольвенции непротиворечив и полон. Непротиворечивость означает, что если когда-нибудь мы придем к пустому предложению, то исходное множество обязано быть неудовлетворимым. Полнота означает, что если исходное множество неудовлетворимо, то, в конце концов, мы придем к пустому предложению.[2]

1.3.2 Методы поиска доказательства в исчислении предикатов

1.3.2.1 Исчисление предикатов при решении задач

Иногда достаточно только знать, следует ли логически правильно построенная формула W из некоторого множества S правильно построенных формул. Если W не следует из S, то, возможно, мы захотим знать, следует ~W из S. Конечно, в силу неразрешимости исчисления предикатов не всегда можно установить, следует ли W из S.

В других приложениях нужно знать значение элемента x (если он существует), при котором данная правильно построенная формула W (содержащая x в качестве переменной) логически следует из некоторого множества S правильно построенных формул. Иными словами, мы хотели бы знать, следует ли логически правильно построенная формула , и если да, то каков тот частный случай переменной x. Проблема поиска доказательства правильно построенной формулы , исходя из S, является обычной проблемой доказательства в исчислении предикатов, но для построения удовлетворяющего частного случая требуется, чтобы метод доказательства был "конструктивным".

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

1.3.2.2 Стратегии перебора

Непосредственное применение принципа резольвенции соответствует простой процедуре полного перебора при построении опровержения. Такой перебор мы начинается множества S, к которому добавляется резольвенты всех пар предложений в S с тем, чтобы образовать множество R. Затем добавляются резольвенты всех пар предложений в R с тем, чтобы образовать множество R(R(S))=R2(S), и т.д. Этот метод перебора как правило непригоден для практики, так как множества R(S), R2(S),… слишком быстро разрастаются. Практические процедуры доказательства определяются стратегиями перебора, применяемыми для его ускорения. Такие стратегии бывают трех типов: стратегии упрощения, стратегии очищения и стратегии упорядочения.[2]

1.3.2.3 Стратегии упрощения

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

Исключение тавтологий.

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

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

Иногда появляется возможность означить (выяснить значение истинности) литералы, и это оказывается удобнее, чем включать соответствующие предложения в S. Такое означивание легко провести для константных частных случаев. Например, если предикатная буква E обозначает отношение равенства, то означивание константных частных случаев типа E(7,3), когда они появляются, провести легко, хотя нам бы не хотелось добавлять к S полную таблицу, содержащих много константных частных случаев литералов E(x,y) и ~E(x,y).

Если какой-нибудь литерал предложения получает значение истинности T, то все предложения можно отбросить, не нарушая при этом свойства невыполнимости оставшегося множества. Если же какой-нибудь литерал при означивании получает значение истинности F, то из этого предложения можно исключить данное вхождение литерала.[2]

Исключение подслучаев.

Предложение называется подслучаем предложения , если существует такая подстановка , что . Например,

- подслучай предложения ,

- подслучай предложения ,

- подслучай предложения

- подслучай предложения .

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

1.3.2.4 Стратегии очищения

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

Про стратегию очищения, использующую критерий C, говорят, что в ней используется "резольвенция по отношению к C". Для применения такой стратегии сначала вычисляется , затем и т.д. до тех пор, пока при некотором n в не окажется пустого предложения обозначемого nil.

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

1.3.2.5 Формы доказательства с отфильтровыванием

Доказательство с отфильтровыванием предшествующих вершин производится с использованием AF-графа. Граф опровержения имеет AF-форму, если каждая из его вершин соответствует одному из следующих предложений:

базовому предложению;

предложению, непосредственно следующему за базовым;

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

Граф в виде лозы представляет собой частный случай графа в AF-форме: каждая из его вершин соответствует либо предложению 1, либо предложению 2. Но граф типа лозы существует не для всех неудовлетворимых множеств. Ниже приведен пример такого графа.[2]

Рис 1.1. Вид графа в AF-форме.

1.3.2.6 Стратегии поддерживающего множества

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

Так как множество S-K удовлетворимо, существует граф опровержения, имеющий AF-форму, у которого верхней вершиной служит один из элементов множества K. Таким образом, стратегия поддерживающего множества полна, поскольку она допускает все резольвенции, допускаемые AF-стратегией.[2]

1.3.2.7 Стратегии упорядочения

На основе резольвенций, обеспечиваемых различными стратегиями очищения, иногда можно искать опровержение, упорядочив выполняемые резольвенции. В стратегиях упорядочения не запрещаются никакие типы резольвенций, а лишь даются указания на то, какие из них надо выполнять в первую очередь. Стратегии упорядочения соответствуют эвристическим стратегиям перебора для поиска на графах. При хорошем упорядочении не обязательно вычислять все элементы множеств R(S), R2(S) и т.д. Если пустое предложение появляется впервые на уровне n, что хочется думать, можно прямо направить на этот уровень, не заполняя нижние уровни.

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

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

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

1.4 Анализ характеристик существующих интерпретаторов

В настоящее время существует несколько интерпретаторов и компиляторов языка Пролог.

Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15