|
b>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 Анализ характеристик существующих интерпретаторов В настоящее время существует несколько интерпретаторов и компиляторов языка Пролог. СиПролог (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] Турбо Пролог (Turbo Prolog). Поставщик Borland Int. Работает под управлением MS-DOS. Является полноценным компилятором, вследствие чего обладает строгим контролем типов. Создан собственный оконный интерфейс с четырьмя окнами: редактор, отладчик, консоль и окно сообщений об ошибках. Сообщения отладчика аналогичны сообщениям отладчика СиПролога.[6] Visual Prolog. Поставщик Prolog Development Center. Работает под управлением Windows 3.1 и выше. Обладает развитым оконным интерфейсом. Позволяет создавать полноценные приложения для Windows с использованием окон. Сообщения отладчика аналогичны СиПролог. Основным недостатком всех рассмотренных диалектов языка Пролог является то, что база данных у них должна храниться в оперативной памяти, либо в виртуальной, когда реальные базы данных могут занимать десятки и сотни мегабайт. Вторым недостатком является то что, ни один из диалектов не поддерживает современные базы данных, а подключает базы данных, содержащиеся в текстовых файлах и представляющих собой, по сути, часть Пролог-программы. 1.5 Необходимость разработки интерпретатора языка ПрологОтсутствие возможности работы с универсальными базами данных у вышеперечисленных версий языка Пролог заставляют разработчиков писать программы на универсальных языках программирования. Вследствие этого, увеличивается время разработки программ для баз данных, так как универсальные языки программирования, такие как С, Паскаль и проч., не имеют удобных встроенных средств работы с базами данных. Также все перечисленные выше версии Пролога имеют недостаточно удобный интерфейс и средства отладки, либо совсем его не имеют, что уменьшает скорость разработки программ на Прологе. 1.6 Выбор языка программированияНа выбор языка программирования влияют следующие факторы: характер решаемой задачи; имеющиеся в наличии системные библиотеки; поддреживаемые компилятором платформы. По характеру решаемой задачи, для программирования интерпретатора требуется язык программирования, позволяющий: гибко работать с динамически выделяемой памятью; иметь объектно-ориентированное расширение; иметь средства обработки исключительных ситуаций; получать высокоскоростной код. Перечисленным требованиям удовлетворяют С++ и Паскаль. До недавнего времени Паскаль (и его диалект Delphi) значительно уступал С++ по возможности формирования высокоскоростного кода. Но теперь в компилятор Delphi 4 был встроен оптимизатор, который позволяет формировать высокоскоростной код. Также в пользу Delphi 4 говорит и то, что он теперь может оперировать с динамическими массивами, то есть с такими массивами, количество элементов которых может меняться в процессе выполнения программы. Borland Delphi 4 генерирует код для операционных систем Windows 95, 98 и NT. Имеет средства визуального построения приложений. 2 Конструкторская часть2.1 Синтаксис программ на Прологе в нотации Бэкуса-НаураПрограмма::=предложение <предложение> Предложение::=утверждение, управляющая команда Утверждение::=голова.проб_символ Голова :- хвост.проб_символ Голова if хвост.проб_символ Управляющая команда::= целевое утверждение <,целевое утверждение>.проб_символ Голова::=целевое утверждение Хвост::=целевое утверждение <,целевое утверждение> Целевое утверждение::=атом|структура Проб_символ::=пробел, возврат каретки[6] 2.2 Общая структура интерпретатораИнтерпретатор языка Пролог состоит из следующих частей: Предкомпилятор; Интерпретатор. Предкомпилятор выполняет перевод исходных данных в объекты интерпретатора. Исходными данными для предкомпилятора являются:
Страницы: 1, 2, 3, 4
|
