Диссертация (1149226), страница 27
Текст из файла (страница 27)
— Springer Berlin Heidelberg, 2012. — Vol. 7650. — P.212–227.147. Tiwari, A. Logical interpretation: Static program analysis using theoremproving / A. Tiwari, S. Gulwani // CADE 2007. LNCS. — Springer Berlin Heidelberg,2007. — Vol. 4603. — P. 147–166.148. Troelstra, A.
S. A History of constructivism in the 20th century. — ITLIPrepublication Series, 1991. — 30 p.158149. Troelstra, A. S.Basicprooftheory(2nded.)/A. S. Troelstra,H. Schwichtenberg. — New York : Cambridge University Press, 2000. — 417 p.150. Troelstra, A. S. Metamathematical investigations of intuitionistic arithmeticand analysis / A. S. Troelstra (ed.) // Lect. Notes Math. — Springer Berlin Heidelberg,1973. — Vol.
344. — 488 p.151. Tsarkov, D. Using Vampire to Reason With OWL / D. Tsarkov [et al.] //The Semantic Web — ISWC 2004. LNCS. — Springer Berlin Heidelberg, 2004. —Vol. 3298. — P. 471–485.152. Vampire'sHomePage[Электронныйресурс].URL:http://www.vprover.org/ (дата обращения: 17.09.2017).153. Voronkov, A. A. A proof-search method for the first-order logic // COLOG88.
LNCS. — Springer Berlin Heidelberg, 1990. — Vol. 417. — P. 327–338.154. Voronkov, A. Deciding K using KK // Principles of KnowledgeRepresentation and Reasoning (KR’2000). — 2000. — P. 198–209.155. Voronkov, A. A. LISS — The logic inference search system // CADE 1990.LNCS. — Springer Berlin Heidelberg, 1990. — Vol. 449. — P. 677–678.156. Voronkov, A. Proof-Search in Intuitionistic Logic with Equality, or Back toSimultaneous Rigid E-Unification // Journal of Automated Reasoning. — 2003.
—30 (2). — P. 121–151.157. Voronkov, A. Theorem proving in non-standard logics based on the inversemethod // CADE-11. LNCS. — Springer Berlin Heidelberg, 1992. — Vol. 607. — P.648–662.158. Weidenbach, C. Towards an Automatic Analysis of Security Protocols inFirst-Order Logic // CADE-16. LNCS.
— Springer Berlin Heidelberg, 1999. — Vol.1632. — P. 314–328.159. Whittle, J. Amphion/NAV: deductive synthesis of state estimation software/ J. Whittle [et al.] // 16th Annual International Conference on Automated SoftwareEngineering (ASE 2001). Proceedings. — 2001. — P. 395–399.159160. Wiedijk, F. Comparing Mathematical Provers // Mathematical KnowledgeManagement, MKM 2003. LNCS. — Springer Berlin Heidelberg, 2003. — Vol. 2594.— P. 188–202.161.
Wiedijk, F. The Seventeen Provers of the World. Foreword by Dana S.Scott. — Springer Berlin Heidelberg, 2006. — 162 p.162. Zamov, N. K. Maslov's inverse method and decidable classes // Annals ofPure and Applied Logic. — 1989. — 42 (2).
— P. 165–194.160ПРИЛОЖЕНИЕ А. ДОКАЗАТЕЛЬСТВА ПРОМЕЖУТОЧНЫХУТВЕРЖДЕНИЙ ИЗ ГЛАВЫ 2Далее приводятся формулировки и доказательства некоторых утвержденийиз главы 2, вынесенные в приложения из-за объемности доказательств.Используются те же термины и соглашения, что и в главе 2.В лемме 2.5 используются спискии, определения которых даны впункте 2.5.1.Лемма 2.5.
Пусть— секвенция с непустым сукцедентом, а— сингулярные секвенции. Пусть также существует выводизв исчислениии правил из списка, который содержит только применения аксиоми в котором правила из списканепосредственно к секвенциямспискасеквенциине применяются(т. е. каждому применению правила изнепосредственно предшествует применение аксиомы или другогоправила вывода).Тогда найдется такая формулапри выполнении условиясеквенции, что для любого мультимножествавыводиз секвенцийможно перестроить в вывод, в котором порядок примененияправил вывода тот же, только могут отсутствовать некоторые примененияправил из списка , трансформирующиеся в тождественные переходы.Доказательство индукцией по построению вывода секвенции .Еслииявляется аксиомой исчисления.
Тогда любая секвенцияявляется аксиомой исчисленияЕсли, то, где, где, также.совпадает с одной из секвенций, тоявляется сингулярнойсеквенцией и уже удовлетворяет требованию леммы.Рассмотрим теперь случай, когда секвенцияправилу из спискаполучена по какому-либо. Примем по индукционному предположению, что леммавыполняется для всех посылок этого применения правила, содержащих более161одной формулы в сукцеденте. При этом будем считать, что секвенциясодержитболее одной формулы в сукцеденте (в случае ровной одной формулы леммастановится тривиальной).Случай 1.
Применение правили,.В этих случаях посылка содержит не более одной формулы в сукцеденте.Рассмотрим, например, применение правилаВ этом случае применением правиласеквенцию, гдеПрименения правилиОбозначим посылку какрассматриваются аналогично.:. По индукционному предположению существуетиз сукцедентавывод секвенцииможно также получить любую.Случай 2. Применение правилатакая формула:, что при условииможно перестроить в вывод секвенции,удовлетворяющий требованиям леммы. Рассмотрим два подслучая.Случай 2.1..Возьмем.Рассмотримтакоемультимножество.
Тогда в новом выводе применение правилатождественным переходом: искомая секвенциясеквенцией,чтостановитсясовпадает с.Случай 2.2.Пустьвыводима из секвенции. Тогдаи, гдесовпадает с.. Тогда секвенция, применением правила:162Случай 3. Применение правилаОбозначим посылку как:. Как в случае 2, по индукционномупредположению найдем такую формулуиз сукцедентавыполняется для этой секвенции с фиксированной формулойСлучай 3.1.Возьмем, что лемма... Рассмотрим такое мультимножество. Если, что выполняется, то этот случай рассматривается аналогичнослучаю 2.1.
Пусть тогда, где. По индукционномупредположению существует вывод секвенцииисчисленииизв, удовлетворяющий требованиям леммы. Поднимаясь снизувверх в этом выводе, будем добавлять в сукцедент каждой секвенции формулу, за исключением посылок применений правил,и, а такжевсех секвенций, входящих в вывод выше этих посылок.В результате аксиомы исчисленияперейдут в другие аксиомы,применения правил вывода перейдут в применения тех же правил, а секвенциине изменятся: в выводе секвенции, как и в выводе секвенцииони могут выступать в качестве посылок только в применениях правилили,.Полученная фигура будет выводом секвенцииСлучай 3.2.Пустьвыводима из секвенции. Тогдаиили.. Тогда секвенция, гдеСлучай 4. Применение правила..
Рассмотрим случай, применением правила::,163Обозначим левую и правую посылки какисоответственно. Поиндукционному предположению найдем такую формулутакую формулуиз сукцедентас фиксированными формуламиСлучай 4.1.илиСлучай 4.2.иПустьи, что лемма выполняется для этих секвенцийи.. Незначительно отличается от случая 3.1.. Тогдаивыводима из секвенцийиз сукцедента,а.. Тогда секвенцияиприменением правила:Таким образом, во всех случаях лемма выполняется для секвенции .Теорема 2.1. Равнообъемность исчисленийзамкнутаясеквенция,соглашению 2.1, аформулойсеквенциясеквенцияформульныйполучается из.
Секвенцияобразкоторойчто секвенциявыводима в GHPC, тос помощью вывода той же или меньшей высоты.выводима ввыводима в GHPC. Необходимо доказать,.Учитывая замечание 2.2, любой выводвсоответствуеттогда и только тогда, когдавыводима в GHPC. Кроме того, есливыводима в—заменой каждого вхождения формулы видавыводима вДостаточность. Секвенциявыводи GHPC.
Пустьв GHPC можно перестроить в, выполнив следующее преобразование дерева вывода.Поднимаясь снизу вверх по дереву вывода, заменим в этом выводе каждоевхождение формулы видаформулойзамену, применения правилиКаждое применение правилазаменяется применением правила. Перед тем, как выполнить этупреобразуются следующим образом.видаисчисления:164при этом вывод посылкизаменяется выводом секвенции(полемме 3.1.2 из [10], эта секвенция также выводима в GHPC, причем с помощьювывода той же высоты).Теперь рассмотрим случай применения правилавидаВоспользуемся леммой 3.1.3 из [10]: так как левая посылка данногоприменения правила выводима в GHPC, то с помощью вывода той же высотывыводима и секвенция.
Заменим вывод левой посылки выводомэтой секвенции, а правую посылку удалим вместе со всеми секвенциями, которыенаходятся выше нее в дереве вывода. Тогда после замены вхождений формул видарассматриваемое применение правила перейдет в применение правилаисчислениягде,и:получаются из ,формулы видаформулойисоответственно заменой каждого вхождения.Наконец, рассмотрим применение правилагде формулане совпадает с. По лемме 3.1.3 из [10] в исчислении GHPCвыводима секвенция, причем с помощью вывода той же высоты,что и левая посылка.
Поэтому исходное применение правиламожно заменить применением правилаисчисления:при этом вывод исходной левой посылки заменяется выводом новой левойпосылки.165В результате указанных преобразований получим фигуру с последнейсеквенцией , содержащую только применения правил вывода исчисленияПоскольку секвенцияне содержити исчислениеобладает свойствомподформульности, то в полученную фигуру не входитиспользуется аксиома.(а значит, не). Индукцией по построению вывода убедимся, чтополученная в результате фигура является выводом секвенциив исчислении. Новый вывод имеет ту же или меньшую высоту по сравнению с исходнымвыводом.Необходимость.
Секвенциясеквенциявыводима в. Необходимо показать, чтовыводима в GHPC.Пусть — выводв исчислении. Поднимаясь снизу вверх по деревувывода, заменим в этом выводе каждое вхождение формулы вида. При этом применения правилиформулойпреобразуются следующимобразом.Каждое применение правилазаменяется применением правилапри этом вывод посылкиисчисления GHPC:заменяется выводом секвенции(используется лемма 2.2).Каждое применение правилазаменяется применением правила:с аксиомой исчисления GHPCв качестве правой посылки.в166В результате этого преобразования выводаотсутствуют формулы видаполучим фигуруи применения правил. Чтобы получить из фигурывывод секвенцииипримененияправила.Тавчасть,исчисленияв исчислении GHPC,осталось только устранить применения правилаРассмотрим такое применение правила, в которойисчисления., что выше него отсутствуюткотораярасположенавышерассматриваемого применения правила, уже является выводом в GHPC.
Тогда потеореме 3.1 из [10] формульные образы посылок выводимы в исчислении HPCА. Гейтинга. Обозначим заключение рассматриваемого применения правила как. С помощью рутинной проверки можно убедиться, что формульный образправиладопустим в HPC, т. е. из посылок любого применения этогоправила в HPC можно вывести его заключение. Значит, формульный образвыводим в HPC и по теореме 3.1 из [10] секвенциязаменим целиком ту часть фигурывыводима в GHPC. Поэтому, которая находится выше секвенции,выводом этой секвенции в GHPC80. Будем повторять указанную процедурупоочередно к оставшимся применениям правиладо тех пор, пока неустраним все такие применения.
Индукцией по построению вывода убедимся, чтополученная фигура является выводом секвенциив исчислении GHPC.Лемма 2.7. Лемма о подсеквенциях. Для каждой секвенции , выводимой висчислениичто, существует такая выводимая в исчислении. При этом если выводвывода, то существует выводввПреобразование применений правилачто в исчислениивывод левой посылки, где. Затем выводв исчислении GHPC, гдебез штрихов так же, какполучается из ). Еслитакже выводима в GHPC.
Если же,содержит n применений правил, содержащий не более n + k примененийлогических правил, где k — число применений правила80секвенцияв исходном выводе.можно выполнить и по-другому. Из лемм 2.6 и 2.5 следует,можно преобразовать в вывод некоторой секвенцииследует преобразовать в вывод соответствующей секвенции(выражения со штрихами получаются из выражений, то по лемме 3.1.3 из работы [10] искомая секвенция, то можно воспользоваться правилом.167Доказательство индукцией по построению вывода в исчислениианалогии с леммами 4.1 и 3.7 из [68].
Каждой аксиомеочевидным образом соответствует такая аксиомаЕсли же, поисчисленияисчисления, чтополучена по некоторому правилу вывода исчисления., то примемпо индукционному предположению, что лемма выполняется для всех посылокэтого применения правила. С учетом замечания 2.1, многие правила выводаисчисленийиотличаются от правил вывода исчислений[68] лишь наличиемиизв правых частях посылок и заключения. Для случаевприменения таких правил непосредственно применимы рассуждения из [68].Поэтому здесь рассмотрим только случаи применения правил, которыеотличаются более существенно. А именно, это правила(отличаются правила вывода в исчисленияхправило вывода в исчисленияхиСлучай 1. Применение правила,и) иисчисления:,,(отличается).По индукционному предположению существует выводимая всеквенциявыводимую в.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
