47097 (588464), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

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

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

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

Непосредственное применение принципа резольвенции соответствует простой процедуре полного перебора при построении опровержения. Такой перебор мы начинается множества S, к которому добавляется резольвенты всех пар предложений в S с тем, чтобы образовать множество R. Затем добавляются резольвенты всех пар предложений в R с тем, чтобы образовать множество R(R(S))=R²(S), и т.д. Этот метод перебора как правило непригоден для практики, так как множества R(S), R²(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-форму, если каждая из его вершин соответствует одному из следующих предложений:

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

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

3. предложению, непосредственно следующему за двумя небазовыми предложениями 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), R²(S) и т.д. Если пустое предложение появляется впервые на уровне n, что хочется думать, можно прямо направить на этот уровень, не заполняя нижние уровни.

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

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

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

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

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

СиПролог (CProlog). Поставщиком является отдел архитектуры Университета Эдинбурга. Эта версия переносится практически на любой 32-разрядный компьютер с операционной системой UNIX. Синтаксис СиПролога совпадает с синтаксисом DEC-10 Пролога. Встроенного редактора не существует. У отладчика имеются всего четыре команды:

Call - вызов первой фразы предиката

Back To - вызов второй и последующих фраз

Exit - процедура выполнена успешно

Fail - система достигла конца множества фраз.[2]

Квинтус Пролог (Quintus Prolog). Поставляется фирмой Quintus Computer Systems Inc. Он Предназначен для ЭВМ под управлением UNIX и VMS. Квинтус Пролог можно запускать либо как самостоятельный процесс, либо через специальный интерфейс с редактором EMACS. Отладчик аналогичен отладчику СиПролога, но обладает большим количеством команд.[2]

Пролог-2. Поставляется фирмой Expert Systems Int. Работает под управлением MS-DOS. Поддерживает свой механизм виртуальной памяти, что позволяет писать программы, работающие с большим количеством данных. Из-за особого механизма виртуальной памяти программу необходимо разбивать на модули и указывать явно, должен ли находится модуль в реальной памяти или возможно его размещение в виртуальной. Имеется встроенный редактор. Отладчик аналогичен отладчику СиПролога.[2]

Эрити Пролог (Arity Prolog). Поставщик Arity Corp. Работает под управлением MS-DOS или совместимой операционной системы. Имеет механизм виртуальной памяти со страничной организацией. Встроенного редактора нет, отладчик аналогичен предыдущим.[2]

Характеристики

Список файлов ВКР