Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 14

Правиломожно применить к секвенции 1,так как секвенция 1 является правильной инепосредственной подформулы вявляется вхождением. Остальные правиланеприменимы к секвенции 1. В результате применения правилаксеквенции 1 получим секвенцию 2.2.Далее,является вхождением непосредственнойподформулы вправило. Однако к секвенции 2 нельзя применятьиз-за ограничения на собственную переменную (переменнаявходит свободно в заключение правила), причем не выполняются обаограничения — как сильное, так и слабое. К секвенции 2 применимо толькоправило, в результате применения которого получим секвенцию 3.3..Теперь к секвенции 3 следует применить правило.

В данном случаевыполняется сильное ограничение на собственную переменную:не входит взаключение. Тем более выполняется слабое ограничение.4..Если применить правилок секвенции 4, то получим искомуюсеквенцию 5.5..Осталось убедиться, что выполняется ограничение на собственнуюпеременную. Сильное ограничение не выполняется, так как переменнаявходит в секвенцию 5. При этом кроме секвенций 1–4 уже невозможно вывести79никакие новые секвенции. Таким образом, формуланевыводима в исчислениис сильным ограничением на собственную переменную, но при этомсеквенциявыводима в GHPC. Значит, полученное исчисление неравнообъемно исчислению GHPC, если разрешить вхождение вырожденныхкванторов в формулу.

Это же верно и для исчисленияс сильнымограничением на собственную переменную.Если же мы будем использовать слабое ограничение на собственнуюпеременную (как в формулировке исчисленияиз пункта 2.5.3), то секвенция5 становится выводимой, так как переменнаясеквенцию 5. Таким образом, формулане входит свободно ввыводима в исчислениисо слабымограничением на собственную переменную, и свойство полноты исчисления ненарушается.Полученный вывод формулыявляется выводом вв исчислении(который одновременнос точностью до имен правил вывода) можно записать сиспользованием имен вхождений подформул из таблицы 2.5. Например,секвенция 3 будет иметь следующий вид:.

В случае объемных формултакой способ записи может быть удобнее, см. раздел 5 работы [68].Тот же вывод в виде дерева выглядит следующим образом:Отметим,правильными.чтовсе–секвенциивприведенномвыводеявляются802.8. Модификации исчисленийСоглашение 2.2. В дальнейшем записьбудет обозначать замкнутуюочищенную формулу без вырожденных кванторов, в которую входят толькосвязки , ,связки, символы кванторов ,и логическая константа,и логическая константа , т. е. не входят. При этом связкаопределяетсястандартным образом через импликацию и «ложь»:Аналогично приведенным в параграфе 2.2 терминам, в которых фигурируетформула, определяются термины–секвенцияправильнаяит.

д.–атом,При–формула,этом–секвенция,аналогичнымобразомпереформулируются леммы, теоремы и другие утверждения из параграфа 2.5.Рассмотрим модификацию исчисленияформул, удовлетворяющих соглашению 2.2. Данная модификация (назовем ее) получается изаксиомгде, предназначенную для выводаудалением правил,и добавлением схемы:обозначает отрицательное вхождение логической константы(каждому вхождениювв формулусоответствует своя аксиома).Доказательство равнообъемности исчисленийотличается от доказательства теоремы 2.4 для исчисленияи GHPC несущественно(в данном случаедоказательство даже упрощается, так как правила вывода исчисленияболееблизки к правилам вывода исчисления GHPC).Теорема 2.5. Равнообъемность исчисленийвыводима в исчислениивыводима в исчислении GHPC.и GHPC.

Формулатогда и только тогда, когда эта формула81Таким же образом можно рассмотреть исчислениеиз, которое получаетсяс помощью тех же модификаций, что и для полученияНа основе исчислений,из.и их модификаций можно сформулироватьсоответствующие интуиционистские исчисления для вывода формул логикивысказываний. Чисто технически переход к логике высказываний заключается вудалении правил переименования, нормализации и правил для кванторов, а такжевиспользованиитолько–секвенциях). При этомпустыхподстановокв–секвенцияхнеобходимость в использовании(илиунификацииестественным образом отпадает.2.9.

ЗаключениеВсе известные автору интуиционистские исчисления обратного метода(например, [139, 68, 106]) являются односукцедентными. Такие логическиеисчисления удобны при реализации практических алгоритмов поиска вывода, онидостаточно хорошо изучены, для них разработан ряд стратегий поиска вывода.Однако многосукцедентные интуиционистские исчисления также находятприменение в математической логике, в основаниях математики [102, 66, 39, 10,73]ивсовременныхпрограммахАЛВ[71].Многосукцедентныеинтуиционистские исчисления ближе к классическим исчислениям и могут иметьбольшее число обратимых правил. В статье [71] показано, что длина выводанекоторых формул в многосукцедентном исчислении может быть существенноменьше длины самого короткого вывода в односукцедентном исчислении.Автоматизация поиска вывода в многосукцедентных исчислениях полезна как вцелях сравнения их на практике с односукцедентными исчислениями, так и вцелях обобщения существующих стратегий на более широкий класс логическихисчислений.Принимая во внимание вышесказанное, в этой главе было построеномногосукцедентное интуиционистское исчисление обратного методадля82вывода замкнутых формул логики первого порядка.

Доказана равнообъемностьисчисленияисчислению GHPC А. Г. Драгалина54. Выводы в построенномисчислении могут содержать секвенции более общего вида по сравнению свыводами в существующих интуиционистских исчислениях обратного метода(например, по сравнению с исчислением).В главе предложены модификации исчисленияи исчисленияА.

Дегтярева и А. Воронкова [68] для вывода формул логики первого порядка иформул логики высказываний. Также рассмотрен пример вывода формулы,иллюстрирующий некоторые особенности поиска вывода с помощью обратногометода Маслова.54Напомним, что равнообъемность исчислений GHPC и HPC (исчисление предикатов Гейтинга) былаустановлена А. Г. Драгалиным [10].83ГЛАВА 3.

РАЗРАБОТКА СТРАТЕГИЙ ПОИСКА ВЫВОДА ДЛЯИНТУИЦИОНИСТСКИХ ИСЧИСЛЕНИЙ ОБРАТНОГО МЕТОДА3.1. ВведениеЧтобы сделать поиск вывода в исчисленииэффективным,необходимопозволяющимиизбежатьдополнитьпорожденияэтии его модификациях болееисчисленияизбыточныхстратегиями,секвенций.Стратегииобратного метода для классической логики и различных неклассических логикбыли предложены в [29, 20, 157, 109, 139, 68, 38, 106] и в других работах.Некоторые из этих стратегий можно напрямую применить к исчислению,адругие требуется адаптировать. Например, стратегии для классической логикимогут быть неприменимы к интуиционистским исчислениям, поскольку в этихисчислениях присутствуют правила с ограничениями на число формул всукцеденте посылки (как в правилеисчисления). В этой главе, вчастности, рассматривается адаптация ряда стратегий, которая заключается виспользовании новых, специфических ограничений на их применение.

Такжепредлагаются новые стратегии для исчисления. Рассматриваемые стратегиитакже применимы к односукцедентному исчислениюА. Дегтярева иА. Воронкова [68], с учетом замечаний 2.1, 2.3 и 2.4.В параграфе 3.2 приводятся основные определения и обозначения. Впараграфах 3.3 — 3.7 рассматриваются различные стратегии и доказывается ихполнота.

В параграфе 3.8 доказывается полнота любой комбинации этихстратегий. В параграфе 3.9 рассматриваются стратегии для модификацийисчисленийи. В параграфе 3.10 приводятся примеры доказательстваформул, поясняющие работу стратегий. В параграфе 3.11 подводятся итоги главы.Основные результаты настоящей главы изложены в статьях [44, 45].843.2. Основные определения и обозначенияСтратегию X будем называть полной для секвенциального исчисления Y,если применение стратегии X не приводит к уменьшению множества выводимыхв этом исчислении секвенций.В этой главе мы будем в ряде случаев пользоваться линейной записьюприменений правил вывода: запись видаправила вывода с посылкамиобозначает применениеи заключением .В этой главе также используются определения и соглашения из глав 1 и 2.3.3. Стратегия поглощения секвенцийБудемговорить,(обозначается как–секвенциячтопоглощает–секвенцию), если существует такая подстановка , чтоОпределенное таким образом отношениена множестве.–секвенцийявляется вполне стандартным (см., например, [109]).Стратегия поглощения для исчислениятакже определяетсястандартным образом: если в процессе поиска вывода получены две такие–секвенциии, что, то –секвенциюразрешается удалить.В работе [6] эта стратегия называется управлением поднаборностью.Следующая лемма используется в доказательстве полноты стратегиипоглощения.Лемма 3.1.Пусть,–формулы,— правильныеиунифицируемы иподстановкаПустьСлучай 1.а— такаяи,и,подстановка,что.