Автореферат (1149225), страница 3
Текст из файла (страница 3)
Антецедент и сукцедент –секвенции являются конечными–формул, т. е. определяются однозначно с точностью до порядкамультимножествамиследования –формул и могут содержать повторяющиеся –формулы.Вдальнейшемвместотермина« –секвенция» можетиспользоватьсятермин«секвенция», если из контекста понятно, о секвенциях какого типа идет речь.обозначает нормальную форму –секвенции , которая получается изЗаписьзаменой каждой –формулыПустьи–секвенция.— –секвенции,называется подсеквенцией–формула–формулойи(пишется), еслии.
Тогда.является правильной, еслиназывается правильной, если все –формулы виявляются правильными.В таблице 1 представлены правила вывода и аксиомы исчисленияправилах, кромеи.. Во всех, посылки являются правильными –секвенциями и не имеютобщих переменных друг с другом;,иобозначают вхождения подформул в9(в томчисле в записях вида,обозначает –атом;ии т. д.). В схеме аксиом— такие переименования, чтонаиболее общий унификатор формулунификатор подстановокВ правилекаждый из символовии.
Подстановка— –секвенция. В правилахна собственную переменную:;— это –секвенция, а. В правилеии—— наиболее общий— переименование.должно выполняться ограничение— это переменная, которая не входит свободно в заключение.Таблица 1. ИсчислениеПравилаиназываются правилами сокращения. Правилаиназываются правилом переименования и правилом нормализации соответственно.Следующая теорема утверждает равнообъемность исчисленияисчислению GHPCА. Г.
Драгалина. Равнообъемность исчислений GHPC и HPC (исчисление предикатов Гейтинга)была установлена А. Г. Драгалиным.Теорема 1. Секвенциявыводима в исчислениив исчислении GHPC выводима секвенциявхождения подформулы вида, гдеформулой.10тогда и только тогда, когдаполучается иззаменой каждогоЛогическое исчислениеявляется многосукцедентным (т. е. правая частьвыводимых секвенций может содержать более одной формулы), в отличие от существующихинтуиционистских исчислений обратного метода. Поэтому исчислениеближе кклассическим исчислениям и позволяет выводить секвенции более общего вида.
В частности,это дает возможность обобщить некоторые стратегии, применимые к односукцедентнымисчислениям обратного метода, на более широкий класс интуиционистских исчислений.Во второй главе также рассматриваются модификации исчислениядляинтуиционистской логики первого порядка и интуиционистской логики высказываний.Например, модификация, в которой вместо отрицания используется логическая константа .Третья глава работы посвящена рассмотрению стратегий поиска вывода для исчисления, позволяющих уменьшить размер пространства поиска вывода.Стратегия поглощения определяется стандартным образом (но при этом используетсяспецифическое отношение–секвенцию(пишется), если,,– еквенцияи, что, торазрешается удалить.состоит из следующих правил вывода:,ипоглощаетдля некоторой подстановки .
Если в процессепоиска вывода получены такие секвенцииПусть список–секвенций).на множестве, а также,,в случае, если формула,,не содержитотрицательных вхождений символа .Стратегия упрощения секвенций для исчислениясеквенциям правила из спискапозволяет применять к, как только эти правила становятся применимы (заисключением нескольких частных случаев, указанных в диссертации). При этом исходныесеквенции удаляются.Стратегия упрощения является адаптированным вариантом стратегий А.
Воронкова дляклассической логики и Т. Таммета для односукцедентного интуиционистского исчисления(«reduction strategy»), при этом используется специфический список «упрощающих» правил.Стратегия удаления секвенций с недопустимыми подстановками (УСНП) являетсяограниченнымвариантомтактикиудалениянаборовснедопустимымисистемамизависимостей, в общем виде сформулированной С. Ю. Масловым.
В диссертационной работеадаптация тактики заключается в выделении частных случаев недопустимых подстановок всеквенциях, проверку которых можно выполнить достаточно быстро.Новая стратегия удаления секвенций с недопустимыми формулами (УСНФ)позволяет обнаруживать секвенции, которые не могут участвовать в выводе формулысуществующих для правил,,,11ииз-заограничений на число формулв сукцеденте посылки. В ряде случаев такие секвенции могут быть выявлены на ранних стадияхпоиска вывода (в диссертации приведены формальные условия недопустимости секвенций).Стратегия тривиального сокращения позволяет сокращать формулы в секвенции(без порождения новой секвенции), если полученная в результате такого сокращения секвенцияпоглощает.
Эту стратегию можно считать аналогом тактики перехода к тривиальнымспецификациям, предложенной С. Ю. Масловым для случая классической логики.В работе отмечается, что все вышеприведенные стратегии также применимы кисчислениюА. Дегтярева и А. Воронкова.Сингулярная стратегия: поиск вывода формулывыполняется в исчисленииА. Дегтярева и А.
Воронкова, полученный вывод преобразуется к выводу в исчислении.Сингулярная стратегия ранее не была представлена в литературе по обратному методу (всуществующих работах используются односукцедентные исчисления).Следующая теорема верна при некоторых естественных ограничениях на применяемыйалгоритм поиска вывода.Теорема 2. Совместимость стратегий. Любая комбинация перечисленных вышестратегий является полной для исчисления.Третья глава также содержит примеры доказательства формул в исчислении,демонстрирующие применение стратегий поиска вывода.Четвертая глава содержит описание алгоритма поиска вывода в исчислении,позволяющего комбинировать стратегии поиска вывода, а также описание программнойреализации этого алгоритма. Алгоритм применим не только к исчислению, но и к другимсеквенциальным исчислениям обратного метода.Предложенный алгоритм представляет собой вариант «given clause algorithm».
Основнаяидея заключается в разделении всех участвующих в доказательстве секвенций на два списка:активные и использованные секвенции. При этом алгоритм работает так, что списокиспользованных секвенций, как правило, имеет относительно небольшой размер, а списокактивных секвенций может разрастаться достаточно сильно. В проверках поглощенияучаствуют только использованные секвенции, что позволяет сократить накладные расходы натакие проверки.
Используется два частных случая стратегии поглощения: стратегии прямого иобратного поглощения. При прямом поглощении удаляется новая секвенция, если онапоглощается одной из использованных секвенций, а при обратном поглощении удаляетсяиспользованная секвенция, которая поглощается новой секвенцией.12На основе предложенного алгоритма разработана программа АЛВ WhaleProver, котораяможет выполнять поиск вывода в исчислении, в оптимизированном варианте исчисления, а также в их модификациях.
Программа разработана на языке C++. Выбор языкаобусловлен следующими факторами: гибкость и универсальность языка, возможностьуправления деталями реализации алгоритма, объектно-ориентированный подход.В диссертации приведены результаты ряда экспериментов с программой WhaleProver назадачах из библиотеки ILTP версии 1.1.2. Все эксперименты проводились на персональномкомпьютере с процессором Intel Core i5 3.40 ГГц, ОС Windows 7 и 16 Гб ОЗУ с лимитомвремени 100 секунд на каждую задачу.В частности, на выборке из 362 задач различной сложности был проведен рядэкспериментов по сравнению стратегий поиска вывода.
Основные результаты для исчисленияпредставлены в таблице 2. Первый столбец таблицы содержит номера экспериментов, вследующих шести столбцах знаком «+» отмечены включенные в экспериментах стратегии, впоследующих столбцах указаны результаты экспериментов. В таблице стратегиям назначенысокращенные наименования: СИ — сингулярная стратегия, TС — стратегия тривиальногосокращения, УП — стратегия упрощения, УСНП и УСНФ — как раньше, ОП — обратноепоглощение. В каждом эксперименте использовалось прямое поглощение, чтобы при любойкомбинации других стратегий программа могла решить все задачи.Таблица 2. Основные результаты сравнения стратегий поиска вывода для№СИ ТС УП УСНП УСНФ ОПэксп.12345678910+++++++++++++++++++++++++++++Средняя Средняявысотадлинавывода вывода19,985,819,485,817,337,06,938,419,586,019,585,85,213,35,214,05,213,35,314,0Средний размерпространствапоиска вывода1242,91248,01042,5189,6998,61004,8106,2104,4105,2103,2Суммарноевремя, сек170,4136,5106,55,673,993,52,72,33,12,8Стратегия упрощения существенно опережает другие стратегии по времени и размерупространства поиска вывода.
Стратегия УСНФ по тем же показателям эффективнеетривиального сокращения. Сингулярная стратегия позволяет уменьшить время решения задач,но эффект от ее использования снижается при включении всех остальных стратегий.13Максимальная эффективность программы достигается при включении всех стратегий(эксперимент 10) или всех, кроме обратного поглощения (эксперимент 8).
Во втором случаевремя решения задач меньше (проверка поглощения является достаточно затратной операцией).Оптимальная конфигурация из эксперимента 8 использовалась при экспериментальномсравнениипрограммыWhaleProverссуществующимипрограммамиАЛВдляинтуиционистской логики на задачах из ILTP. Результаты программы WhaleProver получены всоответствии с руководством по использованию библиотеки ILTP. Результаты других программвзяты с сайта ILTP и из публикаций авторов. На рисунке 1 для всех программ представленазависимость числа решенных задач от лимита времени на каждую задачу.Лимит времени, сек600JProver500ft-Prolog400ileanSePileanTAP300ft-C200WhaleProver100ileanCoP 1.0Imogen00200400600Задач решено800Рисунок 1.
Количество решенных задач при увеличении лимита времениРезультаты программ получены на разных вычислительных машинах. Несмотря на это,сравнение является корректным в соответствии с методикой, рекомендуемой признаннымиэкспертами в области АЛВ. А именно, начиная с некоторой точки, прирост числа решенныхзадач практически прекращается, поэтому результаты программ существенно не изменятся прилинейном увеличении частоты процессора или объема ОЗУ. Дополнительно в диссертацииприводятся результаты программ, для которых нет данных о времени решения каждой задачи.Всего программа WhaleProver решила 811 задач из ILTP (доказала 621 и опровергла 190утверждений). Из них для 650 задач известен их статус в интуиционистской логике, при этомрезультат программы соответствует этому статусу.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
