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

Таким образом,Случайсодержит ровно однуподъемаприменениядопустимо в новой фигуре.правиланадприменениемдвухпосылочного правила также стоит рассмотреть подробнее. Пустьприменением правила,а— применением правилачто предок82 боковой формулы применения правилаприменения правилаявляется. Будем считать,входит в левую посылку(альтернативный случай рассматривается по аналогии).Тогда исходная фигура имеет следующий вид:Мультимножестваисодержат ноль или более вхождений формулы. Двойная линия означает ноль или более применений правила сокращения, врезультате которых мультимножествопереходит вформулой, а формулы из мультимножествтолько над левой посылкой82иявляется пустым, то подниматьсокращаются стребуется.

Рассмотрим подробнее более сложный случай,содержит хотя бы один элемент. Тогдапосылками, мультимножество.Если мультимножествокогдапереходит вподнимается над обеимии преобразованная фигура имеет следующий вид:Формальное определение предка вхождения формулы в вывод см. в статье С. К.

Клини [16].192В новом выводе по-прежнему выполняются ограничения на собственныепеременные, так как вкоторые входят в,в,,имогут входить только те переменные,или вВо всех случаях свойство чистоты переменных в новом выводе продолжаетвыполняться.Лемма 3.6. Рассмотрим вывод  формулысодержащий либо применение правилаиз спискадля исчисления,, либо такое применение правила, боковая формула которого не имеет вид(обозначим указанное применение каквывод входит секвенцияв исчислении). Пусть выше примененияв, к которой применимо то же правило с той жебоковой формулой (которая является предком боковой формулы применения).Тогда вывод  можно перестроить (с сохранением свойства чистотыпеременных, если оно имелось), поднимая наверх применениеего посылкой не окажется .

При этом в случае, когдаправиладо тех пор, покаявляется применением, может потребоваться удвоение применения этого правила, еслионо поднимается над применениями двухпосылочных правил.Как и в лемме 3.5, можно считать, что вывод  обладает свойствомчистоты переменных.Случай 1. Рассмотрим сначала случай, когдаправилаявляется применением:В этом случае секвенцияимеет видвсе секвенции, входящие в вывод междуи посылкой ..

Такой же вид имеют193Назовем рангом вывода число применений логических правил, которыевходят в вывод между секвенциейи посылкой применения правила.Доказательство индукцией по рангу доказательства. Пусть по индукционномупредположению лемма выполняется для выводов с рангом, не превышающим n.Докажем, что тогда лемма выполняется для выводов с рангом n + 1.Рассмотримпредшествующееприменениелогическогоправила,. Из условия леммы следует, чтонепосредственноипринадлежатразличным формулам в заключении второго из них.Рассмотрим случай, когдаявляется применением однопосылочногоправила. Из леммы 3.4 следует, что примененияисключением случаев, когда параприменения правилапеременнойв термможно переставить, засовпадает с, причем собственная переменнаятермиприменения правиламожно заменить новой переменной в посылкеи всюдуне может содержатьвхождений переменной , порождаемых вхождением термасеквенциявходит в.

Однако в указанных случаях вхождениявыше в выводе. При этом секвенциякак иначе правилоили,в посылку, такбыло бы неприменимо к . Тогда после указанной заменыне изменится. Таким образом, по лемме 3.4 можно переставитьпримененияи . Новый вывод имеет ранг, не превышающий n, поэтому можновоспользоваться индукционным предположением и поднять применениетак,как этого требует лемма.Пусть теперьявляется применением двухпосылочного правила.Рассмотрим случай, когдаявляется применением правилабоковой формулы применения правилаправилаи предоквходит в левую посылку применения.

Остальные случаи отличаются несущественно. Рассмотрим частьвывода, содержащую применения правили , между которыми находятся нольили несколько применений правила сокращения:194Обозначения те же, что и в доказательстве леммы 3.4. Будем считать, чтомультимножествосодержит хотя бы одно вхождение формулытребуется поднять применение правилаправила. Пустьнад левой посылкой применения. Преобразованный вывод выглядит следующим образом:Приведенное преобразование уже не является перестановкой по Клини, таккак требуется удвоение применения правила.

Ограничения на собственныепеременные в новом выводе выполняются по тем же причинам, по которым онивыполняются при подъеменад обеими посылками применения правила(этот случай был рассмотрен в доказательстве леммы 3.4). После преобразованиячасть вывода, расположенная над левой посылкой применения правила,имеет ранг не более n.

Поэтому в силу индукционного предположенияприменениеможно поднять желаемым образом.Случай 2.является применением правилаВ этом случаеимеют видправила:и все секвенции, входящие в вывод междуи посылкой ,. Так как по условию леммы боковая формула примененияне имеет вид, то этому применению не может непосредственнопредшествовать применение правила. Поэтомуи(определяется также, как в случае 1) принадлежат различным формулам в заключении второго из195них. Все рассуждения из случая 1 остаются верны, только удвоение примененияправилане требуется, так как междуи посылкойне могут применятьсяправила, главная или боковая (боковые) формулы которых входят в сукцедент.Лемма 3.7.

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

Поэтому применение правила–формулив различные вхождения–формул в конечную секвенцию, которые имеют вид–формулыидляи. Еслине являются боковыми формулами применения. Поэтому для–формули, топродолжает, что и для –формулвыполняться то же условие из определенияив секвенции(см. условие 1) следует, чтоне может быть таким применением правилакоторого являются обе –формулыи. То же верно в случае, когдаявляется применением правилапереименования, нормализации или сокращения.Пусть теперьявляется применением логического правила вывода и однаиз его боковых формул совпадает сили. Рассмотрим три случая, взависимости от того, какое из трех условий из определения множествавыполняется дляи.196Случай 1.

Выполняется условие 1:совпадает с, при этомЕслиилиимеет вид.является боковой формулой применения , топрименением ни одного из правил–формула,не может бытьили,уже входит в сукцедент . Поэтому дляили, так кактакже выполняется. Тем более это верно в случае, когдабоковой формулой примененияи. Тогда еслине являетсяимеет видвыполняется условие 1, а в противном случае для, то дляиивыполняетсяусловие 3.Случай 2. Выполняется условие 2:иимеет вид,,является строго положительным вхождением в .В этом случае(по тем же причинам, что и в случае 1), астрого положительным вхождением всовпадает с. При этом либо.

В первом случае дляиявляется, либовыполняется условие 2, аво втором случае — условие 1.Случай 3. Выполняется условие 3:этом либоне имеет вид, привходят в антецедент, то, либоЕсли обе.–формулыиодновременно выполняются условиякакиявляется положительным вхождением в, либо, так. Поэтому либо. То же верно в альтернативномслучае, когда хотя бы одна из –формуливходит в сукцедент(см.случай 1).Без ограничения общности будем считать, чтоЕслине совпадает сили не является боковой формулойприменения , тоПусть теперьприменения. Тогда длясовпадает с. Тогда если.имеет видивыполняется условие 3.и является боковой формулой(при этомили197), то дляивыполняется условие 1, иначе длявыполняется условие 3.Таким образом, во всех случаяхдоказательство отличается несущественно..

Дляи198ПРИЛОЖЕНИЕ В. ЗАДАЧИ ИЗ БИБЛИОТЕКИ ILTP,ИСПОЛЬЗОВАННЫЕ ПРИ СРАВНЕНИИ СТРАТЕГИЙ ПОИСКАВЫВОДАВ таблице В.1 представлен список задач, которые использовались в главе 4при сравнении стратегий поиска вывода для обратного метода. Определениестатуса и рейтинга задач из ILTP приводится в статье [121]. В таблице указаныпереведенные на русский язык статусы задач: «Теорема» (соответствует статусу«Theorem») и «Не теорема» (соответствует статусу «Non-Theorem»).Таблица В.1. Задачи для сравнения стратегий поиска выводаЗадачаALG198+1GEJ007+4GEJ038+1GEJ042+1GEJ047+2GEJ062+1GEJ064+1GEJ066+1GEJ068+1GEJ072+1GEJ074+1GEJ076+1GEJ078+1GEJ080+1GEJ082+1GEJ084+1GEJ089+1GEJ097+1KRS064+1KRS066+1KRS068+1KRS090+1KRS092+1KRS094+1KRS105+1KRS125+1KRS130+1KRS134+1KRS136+1Статус ILTP Рейтинг ILTPТеорема0,25Теорема0Теорема0,5Теорема0,75Теорема0,75Теорема0,5Теорема0,75Теорема0,5Теорема0,5Теорема0,75Теорема0,75Теорема0,5Теорема0,5Теорема0,75Теорема0,5Теорема0,5Теорема0,75Теорема0,5Теорема0Теорема0Теорема0Теорема0,5Теорема0,25Теорема0,25Теорема0,5Теорема0,5Теорема0,25Теорема0,25Теорема0ЗадачаGEJ002+2GEJ009+4GEJ038+2GEJ047+1GEJ060+1GEJ063+1GEJ065+1GEJ067+1GEJ069+1GEJ073+1GEJ075+1GEJ077+1GEJ079+1GEJ081+1GEJ083+1GEJ085+1GEJ090+1GEO080+1KRS065+1KRS067+1KRS074+1KRS091+1KRS093+1KRS100+1KRS123+1KRS126+1KRS131+1KRS135+1KRS137+1Статус ILTP Рейтинг ILTPТеорема0,5Теорема0Теорема0,25Теорема0,75Теорема0,5Теорема0,75Теорема0,5Теорема0,75Теорема0,5Теорема0,75Теорема0,75Теорема0,5Теорема0,5Теорема0,5Теорема0,5Теорема0,5Теорема0,75Теорема0,75Теорема0Теорема0,25Теорема0,75Теорема0,25Теорема0,25Теорема0Теорема0,5Теорема0,25Теорема0,75Теорема0,25Теорема0199ЗадачаСтатус ILTP Рейтинг ILTPKRS139+1Теорема0KRS164+1Теорема0KRS166+1Теорема0,25KRS169+1Теорема0KRS171+1Теорема0,25LCL230+1Не теорема0MGT022+1Теорема0MGT028+1Теорема0MGT032+2Теорема0MGT041+2Теорема0,25PUZ061+1Теорема0SET027+3Теорема0,75SET046+1Теорема0SET062+3Теорема0SET148+3Теорема0,75SET196+3Теорема0,75SET575+3Теорема0SET583+3Теорема0,75SET602+3Теорема0,75SET605+3Теорема0,75SET786+1Теорема0SWV011+1Теорема0SYJ001+1.002Теорема0SYJ002+1.001Теорема0SYJ002+1.003Теорема0SYJ003+1.002Теорема0SYJ004+1.002Теорема0SYJ004+1.004Теорема0,75SYJ004+1.006Теорема0,75SYJ004+1.008Теорема0,75SYJ004+1.010Теорема0,75SYJ004+1.012Теорема0,75SYJ004+1.014Теорема0,75SYJ013+1Теорема0,5SYJ015+1Теорема0,5SYJ017+1Теорема0SYJ020+1Теорема0SYJ022+1Теорема0SYJ024+1Теорема0SYJ026+1Теорема0SYJ028+1Теорема0SYJ030+1Теорема0SYJ033+1Теорема0SYJ038+1Теорема0SYJ101+1Теорема0ЗадачаСтатус ILTP Рейтинг ILTPKRS141+1Теорема0KRS165+1Теорема0,25KRS168+1Теорема0,25KRS170+1Теорема0,25LCL181+1Не теорема0LCL414+1Теорема0,25MGT022+2Теорема0MGT030+1Теорема0,25MGT036+3Теорема0PUZ060+1Теорема0SET002+3Теорема0,75SET043+1Теорема0SET047+1Теорема0,75SET063+3Теорема0,75SET194+3Теорема0,75SET574+3Теорема0SET576+3Теорема0SET590+3Теорема0SET604+3Теорема0,75SET627+3Теорема0SET788+1Теорема0,75SYJ001+1.001Теорема0SYJ001+1.003Теорема0SYJ002+1.002Теорема0SYJ003+1.001Теорема0SYJ004+1.001Теорема0SYJ004+1.003Теорема0,5SYJ004+1.005Теорема0,75SYJ004+1.007Теорема0,75SYJ004+1.009Теорема0,75SYJ004+1.011Теорема0,75SYJ004+1.013Теорема0,75SYJ004+1.015Теорема0,75SYJ014+1Теорема0,5SYJ016+1Теорема0SYJ019+1Теорема0SYJ021+1Теорема0SYJ023+1Теорема0,25SYJ025+1Теорема0SYJ027+1Теорема0SYJ029+1Теорема0SYJ031+1Теорема0,25SYJ034+1Теорема0SYJ039+1Теорема0SYJ102+1Теорема0200ЗадачаСтатус ILTP Рейтинг ILTPSYJ103+1Теорема0SYJ105+1.002Теорема0SYJ105+1.004Теорема0SYJ107+1.001Теорема0SYJ107+1.003Теорема0SYJ108+1Теорема0SYJ110+1Теорема0SYJ112+1Теорема0SYJ114+1Теорема0SYJ116+1.001Теорема0SYJ116+1.003Теорема0SYJ117+1Теорема0SYJ119+1Теорема0SYJ121+1Теорема0SYJ123+1Теорема0SYJ125+1Теорема0,25SYJ203+1.006Теорема0SYJ204+1.002Теорема0SYJ204+1.010Теорема0SYJ205+1.006Теорема0SYJ206+1.002Теорема0SYJ209+1.002 Не теорема0SYJ209+1.010 Не теорема0SYJ211+1.002 Не теорема0SYJ212+1.002 Не теорема0SYN040+1Не теорема0SYN044+1Теорема0SYN046+1Не теорема0SYN049+1Не теорема0,75SYN052+1Теорема0SYN056+1Теорема0,5SYN058+1Теорема0SYN061+1Теорема0SYN064+1Не теорема0,75SYN066+1Теорема0,75SYN069+1Теорема0SYN079+1Теорема0SYN082+1Теорема0SYN316+1Не теорема0,75SYN320+1Не теорема0,75SYN323+1Теорема0SYN326+1Не теорема0,75SYN329+1Не теорема0,75SYN337+1Не теорема0,75SYN339+1Не теорема0,75ЗадачаСтатус ILTP Рейтинг ILTPSYJ104+1Теорема0SYJ105+1.003Теорема0SYJ106+1Теорема0SYJ107+1.002Теорема0SYJ107+1.004Теорема0SYJ109+1Теорема0SYJ111+1Теорема0SYJ113+1Теорема0SYJ115+1Теорема0SYJ116+1.002Теорема0SYJ116+1.004Теорема0SYJ118+1Теорема0SYJ120+1Теорема0SYJ122+1Теорема0SYJ124+1Теорема0SYJ203+1.002Теорема0SYJ203+1.010Теорема0SYJ204+1.006Теорема0SYJ205+1.002Теорема0SYJ205+1.010Теорема0,25SYJ208+1.002 Не теорема0SYJ209+1.006 Не теорема0SYJ210+1.002 Не теорема0SYJ211+1.006 Не теорема0,25SYN001+1Не теорема0SYN041+1Теорема0SYN045+1Теорема0SYN048+1Не теорема0,75SYN050+1Теорема0SYN055+1Теорема0SYN057+1Теорема0SYN059+1Теорема0,25SYN062+1Теорема0SYN065+1Теорема0SYN068+1Теорема0SYN073+1Не теорема0,75SYN080+1Теорема0,25SYN083+1Теорема0,75SYN318+1Не теорема0,75SYN321+1Теорема0SYN325+1Не теорема0,75SYN327+1Не теорема0,75SYN336+1Не теорема0,75SYN338+1Не теорема0,75SYN340+1Не теорема0,75201ЗадачаSYN341+1SYN346+1SYN356+1SYN358+1SYN360+1SYN362+1SYN364+1SYN367+1SYN369+1SYN371+1SYN374+1SYN377+1SYN379+1SYN381+1SYN383+1SYN385+1SYN387+1SYN389+1SYN391+1SYN394+1SYN396+1SYN398+1SYN400+1SYN402+1SYN404+1SYN406+1SYN408+1SYN410+1SYN412+1SYN721+1SYN724+1SYN727+1SYN730+1SYN732+1SYN915+1SYN919+1SYN922+1SYN924+1SYN926+1SYN928+1SYN931+1SYN933+1SYN937+1SYN941+1SYN944+1Статус ILTP Рейтинг ILTPНе теорема0,75Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0,25Теорема0Не теорема0,75Теорема0Теорема0,5Теорема0,25Теорема0Теорема0Не теорема0,75Не теорема0,75Не теорема0Не теорема0Теорема0Теорема0Не теорема0,75Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0,25Теорема0Не теорема0,75Не теорема0,75Теорема0Теорема0Теорема0,25Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Не теорема0,75Теорема0ЗадачаSYN342+1SYN355+1SYN357+1SYN359+1SYN361+1SYN363+1SYN366+1SYN368+1SYN370+1SYN372+1SYN375+1SYN378+1SYN380+1SYN382+1SYN384+1SYN386+1SYN388+1SYN390+1SYN392+1SYN395+1SYN397+1SYN399+1SYN401+1SYN403+1SYN405+1SYN407+1SYN409+1SYN411+1SYN416+1SYN722+1SYN725+1SYN728+1SYN731+1SYN733+1SYN916+1SYN921+1SYN923+1SYN925+1SYN927+1SYN929+1SYN932+1SYN936+1SYN940+1SYN942+1SYN945+1Статус ILTP Рейтинг ILTPНе теорема0,75Не теорема0,75Теорема0Теорема0Теорема0Теорема0Теорема0Не теорема0,75Не теорема0,75Не теорема0,75Теорема0,25Не теорема0,75Не теорема0,75Теорема0Не теорема0,75Теорема0Не теорема0Теорема0Не теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Не теорема0,75Теорема0Не теорема0,75Не теорема0Теорема0,5Не теорема0,75Теорема0,25Не теорема0,75Теорема0Не теорема0Не теорема0,75Теорема0Не теорема0,75Теорема0Теорема0Теорема0Теорема0Не теорема0,75Не теорема0,75Теорема0202ЗадачаSYN946+1SYN948+1SYN951+1SYN953+1SYN956+1SYN958+1SYN960+1SYN962+1SYN964+1SYN966+1SYN969+1SYN971+1SYN973+1SYN975+1SYN977+1SYN979+1SYN981+1Статус ILTP Рейтинг ILTPТеорема0Теорема0Не теорема0,75Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0,5Теорема0Не теорема0,75Теорема0Теорема0Не теорема0Теорема0Теорема0ЗадачаSYN947+1SYN949+1SYN952+1SYN955+1SYN957+1SYN959+1SYN961+1SYN963+1SYN965+1SYN968+1SYN970+1SYN972+1SYN974+1SYN976+1SYN978+1SYN980+1TOP021+1Статус ILTP Рейтинг ILTPТеорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Не теорема0,75Не теорема0,75Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0Теорема0203ПРИЛОЖЕНИЕ Г.