Диссертация (1149226), страница 6
Текст из файла (страница 6)
Тамметом в середине 1990-х годов на базе одноименной программы для21Дата обращения: 17.09.2017.28классической логики. Про интуиционистскую версию программы Gandalf на сайтеILTP сказано, что она представляется некорректной [144]: может доказыватьложные утверждения или опровергать истинные.Программа Imogen не представлена на сайте ILTP, ее описание приведено встатье [106], а исходный код доступен на сайте GitHub [89].
Авторы провелисобственный эксперимент на задачах из ILTP и получили хороший результат: ихпрограмма решила 857 задач, опередив остальные программы.Опубликованные на сайте ILTP [144] результаты тестирования (отмеченныхв таблице 1.1 «звездочкой») программ АЛВ показывают, что они способнырешить не более 30 % задач из этой библиотеки. Лучший результат показалапрограмма ileanCoP (версии 1.0), решившая 690 задач из 2550.
Для сравнения,программа JProver решила лишь 268 задач. Для программы Imogen, новой версиипрограммы ileanCoP 1.2 и программы nanoCoP-i есть более свежие результатытестирования [106, 111]: эти программы решают около 30 % задач из ILTP.Однако их производительность пока несравнима с производительностьюсовременных «пруверов» для классической логики первого порядка, таких какVampire [122, 152] и E [129, 143]. В качестве косвенного подтверждения этомуможно привести результаты соревнования пруверов CASC-2522 [62]: в категориизадач «FOF»23 программа leanCoP24 2.2 решила 159 из 400 тестовых задач, тогдакак программа E решила 316 задач, а Vampire — 380 задач.Отсюда возникают два вопроса. Во-первых, почему в интерактивные«пруверы» Coq и Nuprl внедрена программа JProver, тогда как имеются болеемощные автоматические «пруверы» для интуиционистской логики? Во-вторых,почему даже лучшие из этих «пруверов» пока не могут конкурировать ссовременными классическими «пруверами»?22CASC расшифровывается как «CADE ATP System Competition».23В категорию «FOF» входят задачи на языке логики первого порядка (с равенством).
Награда в этойкатегории считается самой престижной в соревновании «CADE ATP System Competition».24Интуиционистский «прувер» ileanCoP создан на основе классического «прувера» leanCoP.29На первый вопрос у автора настоящей работы есть следующая версияответа. Программа JProver, судя по всему, специально разрабатывалась дляинтеграции в существующие интерактивные «пруверы», чего нельзя сказать одругих программах из таблицы 1.1. Программа JProver написана на языкеObjective Caml, что облегчает ее интеграцию с Coq и MetaPRL, которые написанына том же языке программирования. Кроме того, в Coq и Nuprl к подключаемымлогическим модулям предъявляются определенные требования.
Например,логическиемодулиNuprlдолжныуметьвыдаватьдоказательствавсеквенциальном стиле, что также предусмотрено в JProver. В то же времяинтеграция «пруверов» общего назначения в Coq и Nuprl сопряжена сдополнительными трудностями25.Ответ на второй вопрос, скорее, лежит в области исторического развитияметодов и программ АЛВ. В настоящее время в наиболее мощных «пруверах» дляклассической логики (включая E и Vampire) используется метод резолюций.
Этотметод не лишен недостатков [99], но за счет своей простоты и относительнойлегкости программной реализации он приобрел большую популярность. Дляметода резолюций разработано множество стратегий поиска вывода, которые ивносят основной вклад в эффективность «пруверов». Однако этот методнапрямую не применим к интуиционистской логике: для его использованиятребуется привести формулу к сколемовской стандартной форме, авинтуиционистской логике не все формулы могут быть приведены к указанномувиду эквивалентными преобразованиями. В интуиционистских «пруверах»используются табличные методы или обратный метод Маслова, но для этихметодов пока не разработаны настолько мощные стратегии, как для методарезолюций.Такжеможнозаметить, что половина представленныхв таблицеинтуиционистских «пруверов» написана на языке Пролог. В то же время дляразработки классических «пруверов» часто используются языки C и C++, что25Тем не менее, эта задача вполне решаема, см.
[96].30объясняется их универсальностью, приемлемым быстродействием, а такжевозможностью управлять деталями реализации. На языке C написаны программыE [129] и Prover9 (прежде Otter) [104], в которых применены многие идеи,ставшие «негласным стандартом» для современных программ АЛВ. ПрограммаVampire, написанная на C++, с 2002 года неизменно побеждает на ежегодномсоревновании «CADE ATP System Competition» в самой престижной категории«FOF».Из всего вышесказанного следует, что задача создания эффективногоинтуиционистского «прувера», способного решать новые задачи из библиотекиILTP, является весьма актуальной.1.5.
Методы поиска вывода для логики первого порядка1.5.1. ВведениеЦельнастоящегопараграфа — рассмотретьосновныеметодыАЛВ,применимые к классической или интуиционистской логике первого порядка,после чего подробнее остановиться на обзоре литературы по обратному методуМаслова и на его особенностях по сравнению с другими методами.Отметим,исчислениичтозадачавысказыванийраспознаванияявляетсявыводимостиNP-полной,авзадачаклассическомраспознаваниявыводимости в интуиционистском исчислении высказываний является PSPACEполной (т.
е. полной для задач с полиномиальной памятью). При этом обе задачиразрешимы за экспоненциальное время. Задачи распознавания выводимости всоответствующих исчислениях предикатов существенно сложнее. Какой быалгоритм поиска вывода мы ни взяли, всегда найдутся такие формулы, длякоторых алгоритм не завершит свою работу. При этом все же существуюталгоритмы, способные гарантированно находить вывод формулы в случае, еслиона действительно выводима. Такие алгоритмы можно разработать для всехметодов поиска вывода, обсуждаемых в этом параграфе.311.5.2.
Метод резолюцийСамым разработанным и широко распространенным методом АЛВ дляклассической логики первого порядка является метод резолюций, который былизобретен Дж. А. Робинсоном в 1965 году [123].Метод резолюций принимает на вход отрицание доказываемой формулы,приведенное к сколемовской стандартной форме (см. [50]) и рассматриваемое какмножество дизъюнктов вида, где— литералы (т. е.атомарные формулы или их отрицания)26.Дляпорожденияновыхдизъюнктовразрешаетсяиспользоватьединственное правило вывода, называемое правилом (бинарной) резолюции:где— атомарные формулы,,общий унификатор формули— литералы,,— наиболее.
Заключение правила резолюции называется(бинарной) резольвентой двух посылок.Чтобы свойство полноты выполнялось для бинарной резолюции, ее нужнодополнитьправиломфакторизации(склейки)дизъюнктов.Факторизациязаключается в сокращении двух унифицируемых литер в дизъюнкте до одной.Несмотря на большую популярность, метод резолюций не лишеннедостатков [99, 84]. Так, в результате приведения формулы к КНФ27 длинаформулы может увеличиться, а ее естественная структура может быть нарушена.Прииспользованииметодарезолюцийдаженанебольшихформулахпространство поиска вывода может разрастаться очень быстро.
В связи с этим дляметода резолюций разработано большое число стратегий поиска вывода,позволяющих уменьшить размер пространства поиска вывода: стратегиямножества поддержки (англ. «set of support strategy»), линейная резолюция,26Дизъюнкт такого вида удобно представлять в виде набора литералованглоязычной литературе используется термин «clause».27Конъюнктивная нормальная форма.. Для таких объектов в32семантическая резолюция и т.
д. Гиперрезолюция является одной из наиболееэффективных стратегий [53]. Одно применение правила гиперрезолюции заменяетнесколько применений правила резолюции.Подробное изложение идей метода резолюций и стратегий для него можнонайти в [50, 53]. В книге [84] метод резолюций рассматривается в контекстеразработки программ АЛВ, с примерами реализации алгоритмов на языкеObjective Caml.1.5.3. Табличные методыК табличным методам28 относится целое семейство методов АЛВ,применимых не только к классической, но и к неклассическим логикам(например, к интуиционистской логике).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
