Диссертация (1149226), страница 22
Текст из файла (страница 22)
Поэтому сравнение на рисунке 4.1 является объективным согласноприведенной методике, несмотря на то, что результаты разных программполучены на разных вычислительных машинах. Из похожих соображений былвыбран лимит времени в 100 секунд для программы WhaleProver: его достаточно,чтобы пройти точку PPP.Также следует отметить, что на рисунке 4.1 представлены только тепрограммы, для которых доступны расширенные результаты тестирования назадачах из ILTP, включающие не только общее количество доказанных иопровергнутых утверждений, но и для всех решенных задач результат (доказанаили опровергнута) и время решения.
Это необходимо для выполнения требованийуказанной методики.Для полноты рассмотрим независимые результаты тестирования (от2016 года) двух программ АЛВ для интуиционистской логики первого порядка,разработанных Дж. Оттеном в Потсдамском университете [111]. Его программа131nanoCoP-i доказала 700 утверждений из ILTP с лимитом времени 10 секунд назадачу. Новая модификация программы ileanCoP версии 1.2 в «полнойконфигурации» доказала 717 утверждений с тем же лимитом времени.
Однако встатье Дж. Оттена отсутствуют некоторые существенные детали. Например,неясно, почему был выбран лимит времени 10 секунд и смогут ли его программырешить большее количество задач при увеличении этого лимита. Также остаетсянеизвестно, сколько задач из ILTP, содержащих интуиционистски ложныеутверждения, могут опровергнуть эти программы.
Для сравнения, программаWhaleProver за 10 секунд способна решить (т. е. доказать или опровергнуть) вобщей сложности 719 задач. Отметим также, что на сайте ILTP нет информации отом, какие именно задачи были решены программами nanoCoP-i и ileanCoP 1.2.Программа ileanCoP 1.2 также тестировалась на библиотеке TPTP версии3.7.0 [112].
В настоящей работе библиотека TPTP не используется длятестирования программы по двум причинам. Во-первых, в отличие от библиотекиILTP, она не содержит «интуиционистский статус» задач, который позволяетопределить, корректны ли полученные программой результаты. Во-вторых, лишьнекоторые из приведенных на рисунке 4.1 программ тестировались на библиотекеTPTP, причем на тех ее версиях, которые на данный момент уже устарели(например, по состоянию на 2017 год после версии 3.7.0 вышло более 10 новыхверсий этой библиотеки).Для всех задач в библиотеке ILTP указан «интуиционистский статус» винтуиционистской логике и «классический статус» в классической логике.Например, «интуиционистский статус» может быть одним из следующих:«Theorem» (теорема), «Non-Theorem» (ложное утверждение), «Unsolved» и«Open»(неопределенный«интуиционистскийстатус)77.статус»неВнекоторыхопределен,егослучаях,можнодажекогдавычислитьиз«классического статуса»: если в классической логике формула является ложной,77Статус«Theorem»(теорема)получаюттезадачи,длякоторыхустановленавыводимостьсоответствующих им формул в интуиционистской логике предикатов, а статус «Non-Theorem» (ложноеутверждение) получают задачи, для которых установлена невыводимость соответствующих им формул.132то и в интуиционистской логике она также будет ложной.
Подробнее о статусахзадач в библиотеках ILTP и TPTP можно узнать в [121, 137].Всего программой WhaleProver решены 811 задач (621 утверждениедоказано и 190 опровергнуто). Из них для 650 задач известен или вычислим«интуиционистский статус», при этом результат программы соответствует этомустатусу. В число этих задач входят 88 задач, которые не были решены ни одной изшести программ, включенных в ILTP: JProver, ft-C, ft-Prolog, ileanSeP, ileanTAP,ileanCoP (версии 1.0).
Если также учесть данные регрессионного тестированияпрограммы Imogen, предоставляемые вместе с исходным кодом на сайте GitHub[89], то программа WhaleProver по сравнению со всеми семью программамирешила 16 новых задач с известным статусом. Например, решены следующиезадачи из области обработки естественного языка, которые содержат ложные (какклассически, так и интуиционистски) утверждения: NLP198+1 (обработкафрагмента текста про «old dirty white Chevy») и NLP223+1 (обработка фразы«Vincent believes that every man smokes…»).
Формулировки многих из этих задачслишком объемны, чтобы привести их в тексте диссертации. Так, формула иззадачи NLP198+1 содержит 193 пропозициональных связки и 80 переменных. Этии другие задачи ILTP доступны на сайте [144].Кроме задач с известным статусом, программа WhaleProver по сравнениюсо всеми другими программами решила 16 новых задач с неопределеннымстатусом (все они доказаны программой). Например, решена задача ALG173+1 изтеории квазигрупп, которая содержит 693 пропозициональные связки. Такжерешена задача из области представления знаний KRS133+1 про онтологию,описывающую семейства рептилий: необходимо показать, что различные классыв онтологии не пересекаются.
Задача содержит 125 формул, которые всовокупности содержат 339 связок и 138 кванторов (всего в файле с задачей более900 строк). Также программа WhaleProver решила 89 задач, у которых не толькостатус не определен, но и по какой-то причине отсутствуют результаты другихпрограмм.133Ряд задач из библиотеки ILTP программа WhaleProver позволяет решитьзначительно быстрее других программ. Например, задачу SET146+3 программыileanCoP 1.0 и Imogen решают более чем за 50 секунд, тогда как программаWhaleProver решила ее за доли секунды. Подробные результаты сравнения см.
вприложении Г.4.7. Интерактивный режимИз предыдущего параграфа видно, что программа WhaleProver показаладостаточно хорошие результаты на задачах из библиотеки ILTP. Однако при этомвыяснилось, что у программы могут возникать трудности с рядом относительнонебольших по размеру задач, например, с задачами, содержащими равенство илибольшое количество связок эквивалентности. Отчасти это связано с тем, что впрограмме не используются специальные техники для эффективной работы сравенствами. Вместо этого задача поиска вывода в (интуиционистском)исчислении предикатов с равенством сводится к задаче поиска вывода в(интуиционистском) исчислении предикатов без равенства, как было описано впараграфе 4.3.
Для обратного метода были предложены специальные техникиработы с равенствами [27, 67, 156], однако исследование их применимости кисчислениюявляется открытой теоретической задачей. Устранение связокэквивалентности может привести к значительному увеличению размера формулы,поэтому исследование возможностей более экономного обращения с этимисвязками также является актуальной задачей.В ряде случаев указанные трудности все же можно преодолеть благодаряналичию в программе интерактивного режима взаимодействия с пользователем. Втаком режиме пользователь может сначала упростить задачу с помощью простыхтактик в стиле Coq [142], а затем уже воспользоваться автоматической тактикойпоиска доказательства.Исходная задача формулируется так же, как было указано в параграфе 4.3: ввиде списка гипотези списка целей.
Задача разбивается на134подзадач, соответствующих целям. При этом решение задачизаключается в последовательном решении всех подзадач, а решение каждойподзадачи сводится к поиску вывода секвенции вида, где.В каждый момент времени доступна только первая по порядку подзадача(называемая текущей), к которой можно применять одну из следующих тактик:1. Тактика «intro». Может быть применена, если целевая формула имеет вид,или,.
Применение тактики эквивалентноприменению одного из следующих правил удаления связок и кванторов(слева от черты стоит текущая подзадача, а справа — результат применениятактики):,,, где,константа, не входящая вив— новая предметная.Данная тактика расширяет одноименную тактику Coq возможностьюудалять эквивалентности.2. Тактика «intros». Заключается в рекурсивном применении тактики «intro»,пока она применима.3.
Тактика «elim_auto». Имеет один аргумент — номер гипотезы, которуютребуется «расщеплять». Если текущая подзадача имеет видгде явно указанная формула— это выбранная гипотеза, то исходнаяподзадача заменяется двумя новыми:имеет вид,и. Если подзадача, то она заменяется новой подзадачейЕсли подзадача имеет вид., то она заменяется подзадачей, где — новая предметная константа.Данная тактика совмещает в себе функциональность тактик «elim», «clear»и «intros» (в случае удаления квантора существования) программы Coq.4.
Тактика «split». Применима, если текущая подзадача имеет видпри этом вместо исходной подзадачи вводятся две новые:,и.1355. Тактика «simplify». Заключается в рекурсивном применении тактик«elim_auto», «intro» и «split». При этом в качестве аргумента тактики«elim_auto» используется номер последней гипотезы.6. Тактика«exists».Имеетодинаргумент — терм.Соответствуетприменению правила удаления квантора :.7. Тактики «rewrite» и «rewrite_right». Имеют один аргумент — номергипотезы. Соответствующая гипотеза должна иметь вид, гдеи— термы, не содержащие переменных. Тактика «rewrite» заменяет втекущей цели все вхождения терманаоборот, заменяеттермомтермом, а тактика «rewrite_right» —.8.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
