Диссертация (1149226), страница 20
Текст из файла (страница 20)
е. возможность при необходимости развернутьпрограмму на различных операционных системах).В программе WhaleProver реализована возможность выполнять поисквывода обратным методом Маслова в следующих интуиционистских логическихисчислениях:;(с учетом замечаний 2.1, 2.3 и 2.4);;.118Также в программе можно использовать модификации всех вышеуказанныхисчислений для вывода формул логики высказываний. Имеется возможностьрасширять программу новыми исчислениями обратного метода, причем необязательно интуиционистскими. Например, в программе также реализованоклассическое исчислениеиз работы [68].Программа WhaleProver позволяет применять и комбинировать всестратегии поиска вывода, приведенные в главе 3.
Таким образом, разработаннаяпрограмма АЛВ дает возможность экспериментально подтвердить корректность исравнить предложенные в главах 2 и 3 исчисления обратного метода и стратегиипоиска вывода.Входными данными программы являются: задача в виде набора гипотез (нелогических аксиом) и одной илинескольких целей, сформулированная на языке логики первого порядка илилогики высказываний (задача вводится пользователем вручную илисчитывается из файла); параметры алгоритма поиска вывода (весовая функция для секвенций,отведенный лимит времени на доказательство и т. д.); параметры логического исчисления (вид самого исчисления, используемыестратегии поиска вывода).Параметрыпрограммызадаютсяспомощьюспециальногоконфигурационного файла.Результатработыпрограммыможетбытьразличным:«формулавыводима»69, «формула невыводима», «превышен лимит времени», «ошибка»и т.
д. В случае установления выводимости формулы печатается полученноедоказательство. Также выдается некоторая статистическая информация.Предусмотрена возможность расширения программы путем добавленияновых стратегий поиска вывода, исчислений обратного метода и даже другихметодов АЛВ.69Имеется в виду формула(), которая соответствует исходной задаче (см.
параграф 4.3).1194.4.2. Внутреннее представление данныхДля экономии памяти в ряде классов программы используется шаблонпроектирования «Приспособленец» [3]: разделяемая несколькими объектамиинформация хранится отдельно, а все создаваемые объекты содержат лишьссылки на эту информацию. Например, для каждого вида логической связки вединственном экземпляре создается структура, хранящая информацию о типелогической связки, ее приоритете, способах символьной записи и т. д.Формулы хранятся в программе в форме древовидной структуры. При этомвсе подформулы доказываемой формулы существуют в единственном экземпляре,а секвенции содержат ссылки на них.
Чтобы иметь возможность напечататьдоказательство в случае установления выводимости формулы, вместе с каждойсеквенцией хранится информация о том, из каких секвенций и с помощью какогоправила она была выведена.Термы хранятся в форме графа, в вершинах которого находятсяфункциональные символы, переменные и предметные константы. Для экономиипамяти и облегчения унификации некоторые совпадающие участки графа (вчастности, вершины, совпадающие с переменными и константами) объединяютсяподобно тому, как это описано в статье [6].4.4.3.
Преобразование формул из текстового вида во внутреннююформуПрограмма WhaleProver считывает формулы в текстовом виде70. Выполнятьобработку формул в таком виде крайне неудобно и неэффективно. Поэтомуформула преобразуется к внутреннему древовидному представлению.Впрограммеиспользуетсяалгоритмтипа«shunting-yard»[69],сиспользованием трех стеков для построения формулы «на лету»: стек операндов(формул), стек операторов (кванторов и логических связок), стек термов.
При70Для записи формул используется синтаксис, близкий к синтаксису программы Prover9 [104].120добавлении нового оператора в стек, все операторы с меньшим или равнымрангом последовательно «выталкиваются» из стека. Процедура «выталкивания»состоит из удаления оператора и его операндов из верхушек соответствующихстеков, формирования новой формулы и помещения ее в стек операндов. Послеокончанияобработкивсеостающиесявстекеоператорыпоочередно«выталкиваются» из стека. Таким образом, преобразование выполняется за одинпроход строки, содержащей формулу.4.4.4. Общая структура классов программыВсе классы программы можно разделить на три основные группы: библиотека классов для выполнения символьных операций: преобразованиеформулисеквенций,применениеподстановок,унификация(дляунификации используется такой же алгоритм, как в программе E) и т.
д.; класс, реализующий основной алгоритм поиска вывода; классы для реализации логических исчислений и стратегий поиска вывода.Все три части программы независимы друг от друга, что дает возможностьизменять реализацию алгоритма поиска вывода (например, применять различныекритерии выбора очередной активной секвенции), не меняя при этом реализациюлогических исчислений. С другой стороны, можно изменять или добавлятьлогические исчисления и стратегии без модификации основного цикладоказательства.
Алгоритмы преобразования формул и секвенций также можнооптимизировать, не затрагивая остальные части программы. Таким образом,программа WhaleProver является достаточно гибкой и расширяемой.4.5. Результаты экспериментов на задачах из библиотеки ILTPС помощью программы WhaleProver был проведен ряд экспериментов назадачах из библиотеки ILTP [121] версии 1.1.2. Все эксперименты проводились на121компьютере с процессором Intel Core i5 3.40 GHz, ОС71 Windows 7 и 16 Gb ОЗУ72(программа запускалась на одном ядре в 32-разрядном адресном пространстве,т.
е. фактический объем используемой оперативной памяти не превышал 2 Гб).В частности, на выборке из 362 задач различной сложности был проведенряд экспериментов по сравнению весовых функций для секвенций, а такжестратегий для исчисленийи. Сравнение проводилось по рядукритериев, включая машинно-независимые. В соответствии со статусом в ILTP,298 тестовых задач содержат формулы, выводимые в интуиционистской логикепервого порядка, а еще 64 задачи содержат невыводимые формулы73. Полныйсписок выбранных тестовых задач см. в приложении В.В экспериментах использовались следующие стратегии поиска вывода:прямое и обратное поглощение, стратегия упрощения, стратегии УСНП и УСНФ,стратегия тривиального сокращения, сингулярная стратегия.
Напомним, чтопрямое и обратное поглощение являются частными случаями стратегиипоглощения, их определения были введены в параграфе 4.2.Во всех экспериментах использовалась стратегия выбора активнойсеквенции «с чередованием»: 30 раз подряд выбирается активная секвенция сминимальным весом, затем один раз выбирается секвенция, которая раньшедругих попала в список активных. Константа 30 была подобрана эмпирически.4.5.1. Определение оптимальной весовой функции для секвенцийПервые две серии экспериментов были проведены с целью определенияоптимальной весовой функции для секвенций.
Результаты экспериментовприведены в таблицах 4.1 и 4.2.В экспериментах сравнивались следующие весовые функции (в таблицахкаждая весовая функция обозначается своим порядковым номером):71Операционная система.72Оперативное запоминающее устройство.73В терминологии статьи [121] задача имеет статус «Theorem» («Non-Theorem»), если установленавыводимость (соответственно невыводимость) содержащейся в задаче формулы.1221. Вес секвенции, которая раньше других попала в список активных, равен 1.Веса остальных секвенций равны 0.2. Вес секвенции равен сумме длин путей до формул секвенции.3. Вес секвенции равен средней длине пути до формул секвенции.4.
Вес секвенции равен минимальной длине пути до формул секвенции.5. Вес секвенции равен числу входящих в нее формул.6. Вес секвенции равен числу символов в текстовой записи секвенции.7. Вес секвенции равен сумме весов формул. Вес формулы равен 2, если еенепосредственная надформула имеет видили,,и равен 1,1 в противном случае74.8. Совпадает с пунктом 7, только веса формул равны 2 и 1.9. Совпадает с пунктом 7, только веса формул равны 2 и 0,9.Таблица 4.1 содержит результаты сравнения весовых функций прииспользовании минимального набора стратегий поиска вывода (когда включенатолько стратегия прямого поглощения). Первый столбец таблицы содержитназвание используемого исчисления.
В остальных столбцах приведено числозадач, которые программа решила при использовании весовых функций 1–9(лимит времени на каждую задачу — 100 секунд).Таблица 4.1. Сравнение весовых функций (минимальный набор стратегий)Исчисление74123456789160312275237306228354355362160313276235306228355356359163316277244305231351355362163317278242306231356357357Знаки «+» и «–» обозначают полярность вхождений соответствующих подформул в().123Таблица 4.2 содержит результаты сравнения весовых функций прииспользовании максимального набора стратегий поиска вывода (все стратегиивключены).
Формат таблицы 4.2 совпадает с форматом таблицы 4.1.Таблица 4.2. Сравнение весовых функций (максимальный набор стратегий)Исчисление123456789323352349340356301360360362293327323336353299360360362325352348342356323360360362314327320328353321360360362Представленные в таблицах 4.1 и 4.2 результаты показывают, что числорешенных задач может существенно зависеть от выбора весовой функции.Например, весовая функция номер 1 в большинстве случаев менее эффективна посравнению с другими функциями, поскольку просто выбирает секвенции в томпорядке, в котором они были добавлены в список активных секвенций.
Тольковесовая функция номер 9 позволяет решить все тестовые задачи прииспользовании исчисленийис минимальным набором стратегий, атакже при использовании любого из четырех исчислений с максимальнымнаборомстратегий.Поэтомуданнуювесовуюфункциюбылорешеноиспользовать во всех дальнейших экспериментах.По таблицам можно заметить явное преимущество весовых функций 7–9над функциями 2–4. Объяснить это можно следующим образом. С одной стороны,функции 2–4 в определенном смысле являются ориентированными на цель(позволяют оценить близость к целевой секвенции), тогда как функции 7–9 такимсвойством не обладают.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
