Диссертация (1149226), страница 8
Текст из файла (страница 8)
Л. Катречко [12]. Работа В. А. Доценко [8]интересна тем, что в ней приведен пример неэффективности применения одной измодификаций обратного метода для логики первого порядка. В статьеН. Д. Петуховой и Т. М. Косовской [47] рассмотрена модификация обратногометода для доказательства выводимости предваренных формул специальноговида в логике предикатов, предложен соответствующий алгоритм установлениявыводимости и приведен пример решения задачи распознавания образов спомощью этого алгоритма.Наряду с монографией [22], работа А. Дегтярева и А.
Воронкова [68] нанастоящее время может считаться одним из ключевых трудов по обратномуметоду. В этой работе идеи обратного метода представлены в ясной и нагляднойформе. Изложение сопровождается множеством важных технических деталей,которые отсутствуют во многих других публикациях по обратному методу (хотянекоторые существенные моменты все же опущены). Авторы демонстрируютприменение «универсального рецепта», идеи которого прослеживаются еще вработе С. Ю. Маслова [24], для построения исчислений обратного метода (для38классической логики первого порядка, интуиционистской логики первого порядкаи для различных модальных логик).Вовторойчасти«резолютивноподобные»статьи[68]модификацииавторыпереключаютсяобратногометода,наобсуждаютальтернативные формулировки исчислений обратного метода, удобные дляпрактической реализации: именованные исчисления и исчисления путей34.
Встатье отмечено, что идею именования подформул предложил еще С. Ю. Маслов,и сейчас она активно используется в современных (резолютивных) программахАЛВ для получения более коротких КНФ. Также в своей работе А. Дегтярев иА. Воронков демонстрируют связь между обратным методом и методомгиперрезолюций (эта связь была отмечена С. Ю. Масловым в [28]), формулируютнекоторые стратегии поиска вывода, приводят обзор наиболее значимых, на ихвзгляд, работ по обратному методу.Кандидатские диссертации по обратному методуАвтору известны три кандидатские диссертации по обратному методу [2,18, 46].
Из них первые две посвящены применению обратного метода кмодальнымлогикам,атретья — исследованиюсложностиалгоритмовустановления выводимости (работающих на основе обратного метода) длячастного случая предваренных формул исчисления предикатов, к которомуможно свести решение некоторых задач искусственного интеллекта.Обратный метод и метод резолюцийМожно проследить связь между обратным методом и методом резолюций[28, 7, 68], которая позволяет переносить тактики с одного метода на другой идаже моделировать метод резолюций средствами обратного метода.
В частности,поскольку сам обратный метод тесно связан с секвенциальными исчислениями,эта связь дает возможность переформулировать доказательства, полученныеметодом гиперрезолюций, в рамках секвенциальных исчислений [68]. Поэтомунекоторые авторы называют обратный метод «обобщенным методом резолюций»34В оригинале используются термины «name calculi» и «path calculi» соответственно.39и соответствующие исчисления называют «резолютивными». По мнениюА.
Дегтярева и А. Воронкова [68], данные термины не вполне корректны, и такиеисчисленияправильнеефактическиониназыватьявляются«резолютивноподобными»,специальнымобразомпосколькусформулированнымиисчислениями обратного метода.Практическому сравнению обратного метода и метода резолюций дляпредваренных формул логики первого порядка посвящена магистерская работаВ.
А. Филипповского [49], в которой развиваются идеи из статей [41–43]. Спрактической точки зрения эти работы имеют общий недостаток: в нихсравниваютсяреализацииобратногометодаиметодарезолюцийбезиспользования стратегий поиска вывода, позволяющих уменьшить пространствопоиска вывода и значительно увеличить эффективность обоих методов.Современные программы АЛВ способны решать сложные задачи во многомблагодаря мощным стратегиям и оптимизациям.Стратегии поиска вывода для обратного методаПервые работы, посвященные стратегиям поиска вывода для обратногометода (С. Ю.
Маслов использует термин «тактики»), включают [29] и [20]. Встатье [29] предложены тактики обратного метода для классической логикипервого порядка, основанные на унификации порядка членов в наборах: тактикаобобщенных поднаборов (пн-тактика), тактика расклеенных наборов (рс-тактика),тактика упорядочения наборов (П-тактика). В [28] рассматривается связь этихтактик с тактиками метода резолюций. В работе [20] указанные тактикирассмотрены более детально в применении к конкретизациям общей схемыметода для логики первого порядка с функциональными символами. В той жеработе предложена тактика поддержки и приведены доказательства полнотыразличных комбинаций тактик.
На основе понятия допустимости [22] можносформулировать тактику использования только допустимых наборов (и удалениянедопустимых). Более наглядно эта тактика объясняется в статье В. П. Оревкова[38], где также подробно рассмотрен алгоритм поиска вывода обратным методомМаслова для предваренных формул логики предикатов.40А. Воронков в статье [157] предложил общий способ адаптации некоторыхстратегий, основанных на стратегии поглощения для метода резолюций, кразличным модификациям обратного метода.
А. Воронков доказал несколькообщих теорем, определяющих условия полноты адаптированных стратегий. Этитеоремы применимы к классической логике первого порядка и к некоторымнеклассическим логикам, в частности, к интуиционистской логике.В работе А. Дегтярева [67] используется основанная на похожих идеяхстратегия для логики первого порядка с равенством, позволяющая объединятьнесколько применений правил в одно с использованием понятия «минимальнойконъюнктивнойнадформулы».Предложеннаястратегияприменимапридоказательстве формул в предваренной нормальной форме без кванторовсуществования. Приведено доказательство полноты этой стратегии.Г.
Е. Минцвстатье[109]предложилнесколькостратегийдляинтуиционистской логики высказываний и интуиционистской логики первогопорядка, а в статье [110] — для модальной логики S4. Однако в той части статьи[109], которая посвящена стратегиям для интуиционистской логики первогопорядка,рассматриваютсястратегиитолькодля«резолютивноподобной»модификации обратного метода.Т. Таммет, ученик Г.
Е. Минца, предложил исчисление обратного метода инесколько стратегий для интуиционистской логики первого порядка [139]. Какотмечают авторы работы [68], исчисление Т. Таммета содержит ошибку. Однакоэто не умаляет значимости результатов, изложенных в статье. В частности,корректность рассмотренных стратегий не подвергается сомнению. В той жеработе Т. Таммет предложил новый класс разрешимых формул интуиционистскойлогики первого порядка и показал его разрешимость средствами обратногометода.
Т. Таммет называет обратный метод «обобщенным методом резолюций»,отсюда и термин «resolution» в названии статьи.41Стратегиям поляризации и фокусировки35, применимым к различнымлогикам, посвящена целая серия работ [64, 63, 117, 106, 107]. Результатыэкспериментов,проведенныхэффективностьэтихавторамистратегий.наОднакоихтестовыхзадачах,совместимостьсопоказалимногимиописанными выше стратегиями пока является открытым вопросом.Программные реализации обратного методаСуществует немного публикаций, описывающих программные реализацииобратного метода. Первая компьютерная программа, доказывающая теоремыобратным методом Маслова, была разработана в 60-е годы сотрудникамиЛенинградского отделения Математического института имени В.
А. Стеклова(ЛОМИ). Программа была написана под вычислительную машину БЭСМ-6 исодержала более 10000 машинных команд [6]. В программе были реализованынекоторые стратегии. Например, блок «управление поднаборностью» работал попринципу, схожему со стратегией поглощения.А. А. Воронков в статье [155] весьма кратко описывает программу подназванием LISS, использующую обратный метод для доказательства теорем вразличных логиках (классической, интуиционистской и др.). Однако деталиреализации в статье отсутствуют.В работе Т.
Таммета [139] приведены результаты экспериментов спрограммой АЛВ, использующей описанные в той же работе стратегии.Эффективность программы сравнивалась с программной реализацией из [124], ина большинстве наиболее сложных тестовых задач лучший результат показалапрограмма из [139]. Однако, судя по замечаниям на сайте ILTP [144], реализацияТ. Таммета может выдавать некорректные результаты (опровергать истинныеутверждения и доказывать ложные).В статье Ш. Маклафлина и Ф.
Пфеннинга [106] описана программа АЛВImogen для интуиционистской логики первого порядка, претендующая на звание35В оригинальных статьях используются термины «polarization» и «focusing» соответственно. Стратегияфокусировки использует обратимость правил вывода секвенциальных исчислений и изначально была предложенадля табличных методов.42наиболее эффективной программы АЛВ для этой логики.
По крайней мерепроведенные авторами эксперименты показали, что их программа способнарешить больше задач из ILTP, чем все программы, представленные на сайте ILTP.Существуют реализации обратного метода для модальных логик [154],интуиционистских модальных логик [107], линейной логики [64, 63] и другихнеклассических логик (например, [70, 117, 95]).Долгое время обратный метод оставался в тени других методов: методарезолюций и табличных методов. Исследованием и развитием метода занималасьлишь небольшая группа коллег С. Ю. Маслова. Однако в последние двадесятилетияинтерескобратномуметодусталпостепенновозрастать.Приложения обратного метода к различным логическим исчислениям активноизучаются как российскими, так и зарубежными учеными. Подводя итог обзоруработ по обратному методу, все же стоит отметить, что практическиевозможности этого метода в настоящее время остаются слабо изученными и егопотенциал еще не раскрыт полностью.1.5.5.
Особенности обратного методаСвойство подформульности секвенциальных исчислений играет ключевуюроль в общей схеме обратного метода, позволяя из потенциально бесконечногочисла аксиом использовать лишь конечное его подмножество. Стоит отметить,чтотребованиеиспользоватьисчисления,обладающиесвойствомподформульности, не является существенным ограничением — большинствологических исчислений этим свойством обладают [22]. Общая схема может бытьконкретизирована для каждой подходящей логики, представляющей интерес сточки зрения автоматизации доказательств.С одной стороны, обратный метод имеет общие черты с другимирассмотренными в этой главе методами.
Обратный метод, как и метод резолюций,является локальным (т. е. использует локальные переменные). Более того,резолютивные выводы можно моделировать с помощью обратного метода43Маслова. Обратный метод также имеет сходства с табличными методами: онприменим к произвольным формулам и имеет тесную связь с секвенциальнымиисчислениями генценовского типа.С другой стороны, обратный метод имеет важные отличия от резолютивныхи табличных методов. Обратный метод строит доказательства «сверху вниз» — отаксиом к доказываемой формуле, тогда как табличные методы строят вывод«снизу вверх» — в противоположном направлении. Табличные методы, какправило, используют глобальные переменные, а обратный метод — локальные.По сравнению с методом резолюций обратный метод имеет более широкуюобластьприменения:онподходитдляустановлениявыводимостинепредваренных формул в классической логике первого порядка, также онприменим к неклассическим логикам.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
