Диссертация (1149226), страница 21
Текст из файла (страница 21)
С другой стороны, функции 2–4 не учитываютособенности двухпосылочных правил вывода: эксперименты на задачах из ILTPподтверждают, что частое применение таких правил приводит к резкому124неконтролируемому росту пространства поиска вывода. В то же время функции7–9 позволяют двигаться к цели «по пути наименьшего сопротивления», избегаяповозможностичастогоприменениядвухпосылочныхправилвывода.Использование этих весовых функций позволяет поддерживать более компактноепространство поиска вывода, что помогает решить больше задач.Можно заметить, что при использовании максимального набора стратегийисчисленияи, в которых используется логическая связкабольшинстве случаев не проигрывают исчислениями, всоответственнопо числу решенных задач.
При использовании весовых функций 1–3 исчисленияиоказываютсяявноодносукцедентные исчисленияиисчисленийипредпочтительнее.Еслисравниватьс многосукцедентными исчислениями, то в ряде экспериментов использование односукцедентныхпозволяетувеличить число решенных задач. Рассмотреннаятенденция подтверждается приведенным далее сравнением стратегий поискавывода.4.5.2. Сравнение стратегий поиска вывода для исчисленияРезультаты сравнения стратегий для исчисленияпредставлены втаблице 4.3. Рассмотрены случаи использования отдельных стратегий и основныхих комбинаций.
Первый столбец таблицы 4.3 содержит номера экспериментов, вследующих шести столбцах знаком «+» отмечены включенные в экспериментахстратегии, в последующих столбцах указаны результаты экспериментов75. Длякомпактного представления результатов стратегиям назначены сокращенныенаименования: СИ — сингулярная стратегия, TС — стратегия тривиальногосокращения, УП — стратегия упрощения, УСНП и УСНФ — как раньше (см.пункты 3.5.1 и 3.5.2), ОП — обратное поглощение. В каждом эксперименте75Напомним, что сложностью вывода называется число различных секвенций в дереве вывода, а длинойвывода — число всех секвенций в дереве вывода.125использовалась стратегия прямого поглощения, чтобы при любой комбинациидругих стратегий программа могла решить все 362 задачи.Таблица 4.3.
Сравнение стратегий поиска вывода для№ С Т У УС УС Оэксп. И С П НП НФ П123456789101112131415161718192021222324++++ ++ +++++++++++++++++++++++++++++ ++++++ ++ ++++ ++ +Для++++++++++++++++расчета+Средняявысотавывода19,917,37,119,919,95,25,219,417,36,919,519,55,217,417,36,96,919,55,25,217,46,95,25,3значенийСредняясложностьвывода34,931,214,634,934,911,311,434,531,514,334,634,511,331,531,514,314,334,611,311,331,514,311,311,4суммарногоСредняя Средний размерСуммарноедлинапространствавремя, секвывода поиска вывода85,81242,9170,434,6942,9114,938,6219,28,186,01047,2118,985,8852,573,413,3106,22,713,3105,23,185,81248,0136,537,01042,5106,538,4189,65,686,0998,673,985,81004,893,514,0144,23,937,2869,365,537,0822,370,038,4176,94,838,4143,53,585,9781,046,614,0135,13,414,0109,72,637,2672,238,338,4136,03,214,0104,42,314,0103,22,8времениработыпрограммы,приведенных в последнем столбце таблицы 4.3, каждый эксперимент повторялся50 раз, при этом 95 % доверительный интервал не превышал 3 % от каждого изуказанных значений.В таблице 4.3 при определении высоты, длины и сложности выводов неучитываются применения правил переименования и нормализации, так как впрограмме в случае применения этих правил изменяется существующаясеквенция, а не порождается новая.
При этом в столбце «Средняя высота вывода»126учитываются и высоты деревьев вывода для выводимых формул, и высотыдеревьев поиска вывода для невыводимых формул.Эксперименты 2–5 и 9–12 показывают, что стратегия упрощениясущественно опережает другие стратегии по основным оцениваемым критериям(время и размер пространства поиска вывода). Стратегия УСНФ оказалась по темже показателям эффективнее некоторых других стратегий: это видно присравнении результатов эксперимента 5 с экспериментами 2 и 4, а такжеэксперимента 12 с экспериментом 9.Сравнение экспериментов 1 и 8, 2 и 9, 3 и 10, 4 и 11, 6 и 23, 7 и 24показывает, что сингулярная стратегия позволяет уменьшить время решениязадач. При этом эффект от использования этой стратегии максимален, когдадругие стратегии отключены, и уменьшается при включении всех остальныхстратегий.
Приведенная тенденция нарушается в экспериментах 5 и 12, что можнообъяснить тем, что стратегия УСНФ дает значительно более сильный эффект длямногосукцедентного исчисления, чем для односукцедентного исчисления.Действительно, средний размер пространства поиска вывода в эксперименте 5 на15 % меньше, чем в эксперименте 12.Максимальная эффективность программы достигается при включении всехстратегий (эксперимент 24) или всех, кроме обратного поглощения (эксперимент23). При этом отключение обратного поглощения, хоть и приводит к увеличениюпространства поиска вывода, но позволяет даже уменьшить время решения задач.Объяснить это можно тем, что проверка поглощения является достаточнозатратной операцией.4.5.3. Сравнение стратегий поиска вывода для исчисленияРезультаты сравнения стратегий поиска вывода для логического исчисленияпредставлены в таблице 4.4.
Эксперименты проводились при тех жеусловиях, что и эксперименты из таблицы 4.3. Формат таблицы 4.4 и методырасчета идентичны таблице 4.3.127Таблица 4.4. Сравнение стратегий поиска вывода для№ С Т У УС УС Оэксп. И С П НП НФ П123456789101112131415161718192021222324++++ ++ +++++++++++++++++++++++++++++ ++++++ ++ ++++ ++ ++++++++++++++++++Средняявысотавывода19,617,07,719,619,65,75,719,217,17,519,319,25,817,117,17,57,519,35,85,817,27,55,85,8Средняясложностьвывода35,331,816,435,435,313,113,135,132,016,235,135,113,132,132,016,216,235,113,213,132,216,213,113,2Средняя Средний размерСуммарноедлинапространствавремя, секвывода поиска вывода85,01677,8296,035,31349,7255,340,1272,714,085,11464,0160,684,91326,9235,015,1151,35,415,1150,36,886,81405,4197,538,11215,5195,840,8219,610,886,91207,0130,286,81178,0167,516,4176,18,538,31049,6121,338,11003,6155,740,8203,68,840,8174,26,886,91000,4110,016,4164,26,216,4140,86,038,3857,085,740,8165,76,616,4133,05,216,5131,85,8Видно, что в таблице 4.4 прослеживаются те же закономерности, что былиприведены в пункте 4.5.2 при анализе таблицы 4.3.
Различия имеются вэксперименте 5: для исчислениястратегия УСНФ оказалась не такэффективна на тестовых задачах, как для исчисления. Кроме того, во всехэкспериментах средний размер пространства поиска вывода и суммарное время втаблице 4.4 больше соответствующих показателей из таблицы 4.3. Например, вэксперименте 1 из таблицы 4.4 суммарное время работы программы составляет296 секунд, тогда как в эксперименте 1 из таблицы 4.3 это время составляет чутьболее 170 секунд.
Это можно объяснить тем, что правилоявляется однопосылочным, а правилоисчисленияисчисленияявляется128двухпосылочным. Поэтому замена формул видаформулами видаприводит к увеличению количества переборов.4.6. Сравнение программы WhaleProver с существующимипрограммами АЛВ для интуиционистской логики первого порядкаПрограмма WhaleProver была протестирована на библиотеке ILTPверсии 1.1.2 с целью проверки корректности и сравнения с существующимипрограммами АЛВ для интуиционистской логики первого порядка.На рисунке 4.1 представлено сравнение программы WhaleProver ссуществующими программами по количеству решенных задач из ILTP.Программа WhaleProver показала результат, сравнимый с результатамилучших аналогов: решила 811 задач, доказав 621 утверждение и опровергнув 190утверждений.9008007006005004003002001000ОпровергнутоДоказаноРисунок 4.1.
Сравнение программы WhaleProver с существующими аналогамиПритестированиипрограммыWhaleProverиспользоваласьтажевычислительная машина, что указана в параграфе 4.5. На каждую задачу былвыделен лимит времени 100 секунд. При этом использовалась оптимальная129конфигурация программы, как в эксперименте 23 из таблицы 4.3, с небольшимидополнительнымиоптимизациями.Результатыпрограммыполученывсоответствии с руководством по использованию библиотеки ILTP [121]. Кисходным формулировкам задач применялось только преобразование синтаксисаи добавление аксиом для равенства с помощью стандартной утилиты tptp2X76, чтодопускается вышеуказанным руководством.Другие программы тестировались с лимитом времени 600 секунд наразличных конфигурациях компьютеров: Imogen на 2.4 Ghz Intel Macintosh, Darwin 9.6.0, 2 Gb ОЗУ; все остальные (мы называем их программами, включенными в ILTP) накомпьютере с Xeon 3.4 GHz, Mandrake 10.2 (объем ОЗУ на сайте ILTP неуказан).Результаты программы Imogen взяты из статьи [106] и из результатоврегрессионного тестирования, предоставляемых вместе с исходным кодом [89].Результаты программ, включенных в ILTP, взяты с сайта ILTP [144].Важно отметить, что приведенное сравнение соответствует методике,рекомендуемой признанными экспертами в области АЛВ [136].
В основе этойметодики лежит наблюдение, что у каждой программы АЛВ существует такназываемая точка PPP (Peter Principle Point), после которой прирост числарешаемых задач начинает резко уменьшаться. Это наглядно демонстрируетрисунок 4.2, на котором для участвующих в сравнении программ представленазависимость количества решенных задач от установленного лимита времени накаждую задачу. В соответствии с методикой, результаты программы считаютсядостоверными, если предоставленных программе вычислительных ресурсов былодостаточно для достижения точки PPP. Авторы приводят следующий аргумент впользу своей методики: если программа достигла точки PPP (определить это76Преобразование синтаксиса необходимо, чтобы перевести формулы из формата TPTP в формат,используемый в программе WhaleProver.
Так как в программе не реализованы специальные алгоритмы для выводаформул с равенством, то к посылкам требуется дополнительно добавлять аксиомы для равенства. При этомутилита tptp2X формирует аксиомы в соответствии с § 73 книги [13].130можно путем качественной оценки кривой), то линейное увеличение частотыпроцессора или объема ОЗУ не сможет привести к существенному увеличениючисла решенных задач.Лимит времени, сек600JProver500ft-Prolog400ileanSeP300ileanTAPft-C200WhaleProver100ileanCoP 1.0Imogen00200400600Задач решено800Рисунок 4.2. Количество решенных задач при увеличении лимита времениУ всех сравниваемых программ точка PPP явно достигается менее чем за600 секунд.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
