Динамические логики доказательств с оператором доказуемости тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

ООНОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

: им. М. В. ЛОМОНОСОВА ■ ; 0&

МЕХЛН^^О-МАТЕМАТИЧЕСКИЙ ФАКУЛЬТЕТ

На правах рукописи УДК 510.64

СИДОН ТАТЬЯНА ЛЕОНИДОВНА

ДИНАМИЧЕСКИЕ ЛОГИКИ ДОКАЗАТЕЛЬСТВ С ОПЕРАТОРОМ ДОКАЗУЕМОСТИ

1.01.06 — математическая логика, алгебра и теория чисел

Автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

Москва — 1997

L/it Ш/

Работа выполнена на кафедре математической логики и ории алгоритмов механико-математического факультета ? сковского государственного университета им. М. В. Ломо сова.

Научный руководитель — доктор физико-математическк

наук, профессор С. Н. Артемо Официальные оппоненты — доктор физико-математически

наук, В. П. Оревков — кандидат физико-математичес наук, Л. Д. Беклемишев Ведущая организация — Институт математики

Сибирского отделения Российской академии наук

Защита диссертации состоится ......199/

в 16 ч. 05 мин. на заседании диссертационного совета Д.053.0, при Московском государственном университете им. М. В. I моносова по адресу: 119899, ГСП, Москва, Воробьевы гор МГУ, механико-математический факультет, аудитория 144 С диссертацией можно ознакомиться в библиотеке механш математического факультета МГУ (Главное здание, 14 этаа Автореферат разослан ". Ж.» ..Ш^хгЛ...... . 1997 г.

Ученый секретарь

диссертационного совета

Д.053.05.05 при МГУ

доктор физико-математических наук,

профессор В. Н. Чубарик

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Идея изучения доказуемости сред-гвами модальной логики была впервые сформулирована К. Геделем [1]. Он предложил понимать модальную формулу ПЛ как утвержде-ие о доказуемости А. В качестве логики, аксиоматизирующей есте-гвенные свойства доказуемости, Гедель сформулировал систему 54.

При дальнейшем уточнении доказуеиостной семантики для мо-злыюсти было предложено считать, что □ выражает выводимость некоторой формальной системе, например в арифметике Пеано РА. огда естественным образом возникает определение доказуемост-интерпретации модального языка в арифметический, при ко-эрой оператору □ соответствует стандартная геделевская формула сказуемости Provable(-). Логика 54 оказалась некорректной отно-1тельно такой интерпретации. В [2] Р. Соловеем было показано, го множество формул, выводимых в РА при любой интерпретации, звпадает с логикой Геделя-Леба GL, а также построена логика 5, ароматизирующая модальные принципы, истинные в стандартной одели арифметики.

Логики формальной доказуемости Соловея оказались несовместными с логикой Геделя 54. Причина этого кроется в искажении зойств доказуемости, возникающем на этапе арифметического ко-ирования и связанном с некатегоричностью формальной арнфме-iiKJi. А именно: арифметическое предложение Provable([<р]) озна-ает "существует доказательство х формулы ф", и это х может ока-1ться нестандартным числом. Поэтому Provablt([ip~\) слабее нефор-ального утверждения о доказуемости ф.

Новый подход, предложенный С. Н. Артемовым в [3], состоял в ом чтобы сделать объектом изучения предикат доказательств "р сть доказательство теоремы F". Для этого пропозициональный зык был расширен переменными по доказательствам pi. В арнф-етнческой интерпретации этим переменным соответствуют нату-

'Gödel К. Eine Interpretation des intuitiomstischen Aussagenkalkuls / Ergebnisse Math. Colloq. — 1933. — pd. 4, P. 39-40.

2Solovay R.M. Provability interpretation of modal logic // Israel Jour-al of Mathematics. — 1976. — Vol. 25. — P. 287-304.

3Artemov S., Stra/Зеп T. The Basic Logic of Proofs // Lect. Notes in lomp. Sei — 1993. — Vol. 702. — P. 14-28.

ральные числа — коды индивидуальных доказательств. Формулы представляющие отношение ир есть доказательство формулы F" обрадуются при помощи оператора доказательств [•)(•) согласш правилу: если F — формула up — переменная по доказательствам то [p]F — формула. В [3] были построены разрешимые арифме тически полные системы, аксиоматизирующие свойства различны} классов предикатов доказательств (т.е. фактически классов эффек тивных кодировок выводов в РА). В работе [4] минимальны!: язык логики доказательств был расширен оператором доказуемости □ и сформулированы системы В, J7, М, Вы, и Мы, которые дают совместное описание свойств формальной доказуемости и предикатов доказательств. Логики В, J- и ЛЛ аксиоматизируют соответственно свойства произвольных предикатов доказательств, функциональных предикатов и стандартного геделевского предиката, которые можно обосновать средствами РА. Логики В", Ти и Мш формализуют принципы, истинные в стандартной модели при интерпретациях, основанных на предикатах доказательств соответствующих классов.

Динамическая логика доказательств CP была введена в [5]. В ней квантор существования по доказательствам, содержащийся в □, заменяется на явный терм, содержащий полную информацию о доказательстве. Такие термы строятся из переменных по доказательствам при помощи функциональных символов (двуместные х, + и одноместный !), представляющих рекурсивные операции над доказательствами. Эти операции описываются следующими условиями:

Opl р](Л В) ->■ ([sfl.4 ítx sjß)

Ор2 \t]A \ЩЩА

ОрЗ МЛ fí + а]Л, ИЛ + a]A.

Система CP, построенная в [5], обладает следующими свойствами:

Арифметическая полнота. CP аксиоматизирует множество формул, доказуемых в РА (истинных в стандартной модели) при всех арифметических интерпретациях, основанных на нормальных

4Artemov S. Logic of Proofs // Annals of Pure und Applied Logic. — 1994. — Vol. 67. - - P. '29 59.

5 Artemov S. Operational modal logic. Techii. Rep. No 95 29. — Mathematical Science Institute, Cornell University, 1995.

недетерминированных предикатах доказательств (т.е., неформально говоря, таких, для которых могут быть определены рекурсивные операции, реализующие х, -f и !).

Рункциопамния полнота. Динамическая логика доказательств реализует в виде ^-термов все операции над доказательствами, допускающие пропозициональное описание в арифметике.

''еализацил 54. Модальным аналогом динамической логики доказательств при Р-переводе, состоящем в замене всех вхождений j[t] на □, является 54. Перевод всякой £Р-теоремы доказуем в 54, и обратно, всякая формула, выводимая в 54, является О-переводом некоторой теоремы СР.

Цель работы. Построить п изучить динамическую логику оказательств, дающую совместное описание формальной доказуе-;ости и вычислимых операций над доказательствами, допускающих ропозициональное описание.

Исследовать возможность эффективного описания свойств предн-атов доказательств в языке первого порядка с оператором доказа-ельств.

Методы исследования. В диссертации использованы методы остроения канонической модели и погружения ее в арифметику, совершенствованные автором, а также стандартная техника полу-ения нижних оцсчюк сложности предикатных логик, соответствую-щх арифметическим теориям, основанная на теореме Тенненбаума единственности рекурсивной модели формальной арифметики.

Научная новизна работы. Все результаты диссертации является новыми.

Найдена естественная аксиоматизация динамической логики до-азательств с оператором формальной доказуемости. Полученная истема М.СР включает в себя как логику доказуемости Соловея !L, так и динамическую логику Артемова СР. Наличие модально-ги □ в языке позволило ввести две новые элементарные операции ад доказательствами. Установлена разрешимость, арифметическая функциональная полнота конечных расширений базисного фраг-[ента системы MCP.

Дано определение сильного и слабого варианта интерполяцнон-ого свойства Крейга для логик доказательств. Описаны логики оказательств, обладающие интерполяционным свойством.

Получены нижние оценки сложности предикатно» логики доказа тельств, показывающие невозможность эффективного описания свой предикатов доказательств в языке первого порядка.

Теоретическая и практическая ценность. Работа носш теоретический характер. Ее методы и результаты могут быть по лезны специалистам в области логик доказуемости и теоретическо1 информатики.

Апробация работы. Основные результаты, полученные i диссертации, докладывались на семинаре "Теория доказательств' (руководители семинара — профессор С. Н. Артемов и к.ф.-м.н JI. Д. Беклемишев), на семинаре лаборатории математической логик! ПОМИ и на международных конференциях "Логические основанш информатики" LFCS'94 (г. Санкт-Петербург), LFCS'97 (г. Ярославл] и 10 Международном конгрессе по логике, методологии и фнлософш науки (Флоренция, 1995).

Публикации. Результаты диссертации опубликованы в четы рех работах автора, перечисленных в конце автореферата.

Структура и объем работы. Диссертация состоит из вве дения и трех глав, разбитых на десять параграфов. Список лите ратуры содержит 21 наименование. Общий объем диссертации 7' страниц.

СОДЕРЖАНИЕ РАБОТЫ

Во введении приводится обзор работ, посвященных исследуемо! теме, и кратко формулируются основные результаты диссертации.

В главе 1 построена система М CP динамической логики доказа тельств с оператором формальной доказуемости.

В § 1.1 приведено определение системы MCP и доказаны просты! свойства выводимости в этой системе. Рассматривается язык СРа содержащий два сорта переменных и констант:

• переменные по предложениям So, Sly S^,... и булевы константь Т и

• переменные по доказательствам p0,pi,p2, ■ • ■ и аксиомные кон станты «о, ..........

Термы языка СРа образуются из переменных по доказательствам j аксиомных констант с помощью функциональных символов для one раций над доказательствами: двуместных х, + и одноместных !, ft

и Множество формул содержит переменные по предложениям и эулевы константы, замкнуто относительно булевых связок н модального оператора □, а также если ^ — формула и I — терм, то — формула, называемая д-атомарной.

Аксиомы логики МСР$ разбиваются на две группы: аксиомы логики доказательств С. Н. Артемова В (см. [4]) и операторные акси-эмы, описывающие операции над доказательствами:

аксиомы системы В

ВО все тавтологии

В1 С1(Л В) -» (ОЛ -

В2 а(ал Л) ал

ВЗ ЩЛ->А

В4 ЩЛ ПЩЛ

В5 -.[ijA-> D-i[i].4

операторные аксиомы

Ор1

□ ß) Ор2 ОрЗ

Ор4 Ор5

и (Л В) (ИЛ МЛ [!ф]Л

Мл [i + б1л

[I + s]A [ija4 *]Л

ЩА [ftQ t]OA

MB)

Правила вывода системы МСРц:

(R1)

Л, А -> В В

(R2> А

(R3) ^

Аксиомпая спецификация AS есть конечное множество формул вида [а|Л, где а — аксиомпая константа, Л — одна из аксиом МСР$. Система МСРлц получается добавлением акспомной спецификации 45 к списку аксиом для МСР$. Рассматриваются также логики имеющие в качестве аксиом все теоремы MCP лз и все формулы вида ОЛ —> Л, и единственное правило вывода modus ponens.

В § 1.2 описана арифметическая интерпретация языка CPq и до-сазана лемма о корректности введенных систем. Рассматривается хрифметпка, содержащая ¿ термы (см. [6]), то есть для каждой арифметической формулы ip выражение iz.tp есть терм. Через /iz.ip обозначим «-терм, определяемый формулой <p(z) Л Vu < г-нр(и). Терм uz.ip называется рекурсивным, если уэ(г) AVi> < z->tp{v) есть доказуемо Ei-формула. Если РА Ь 3ztp(z), то терм /«г.9 называется доказуемо тотальным. Замкнутый рекурсивный терм — это доказуемо

6Гильберт Д., Бернайс П. Основания математики. Логические счисления и формализация арифметики. — М., Наука, 1982.

тотальный рекурсивный терм pz.tp, где не содержит других свободных переменных помимо г.

Определение. Стандартным предикатом доказательств называется доказуемо Дрформула Рг/(х,у), такая что формула Рг(у) = 3xPrf(x, у) определяет предикат доказуемости, удовлетворяющий ycj виям Гильберта — Бернайса — Леба [7]:

1) РАН у? РАН Рг(|У|);

2) РА Ь РгЦ<р VI) (Рг(|р|) Рг(Г01));

3) PAhPrirvD^FriWH)!),

где [</>] обозначает геделев номер формулы у. Стандартный предикат доказательств называется нормальным, если для всякого п 6 и множество Т(п) = {А | Prf(n, [Л])} конечно, и функция Т(п) = " код множества Т(/г)" рекурсивна и тотальна. Если при этом для всякого конечного множества Т теорем РА найдется число », такое что Т С T(ii), то Pif(x,y) — нормальный недетерминированный предикат доказательств.

Для всякого нормального недетерминированного предиката доказательств Prf можно построить рекурсивные термы е(х, у), т(х,у), с(х), г(х) и п(х), удовлетворяющие операторным аксиомам (Opl)-(Ор5). Этот факт позволяет определить арифметическую интерпретацию языка CP □.

Определение. Арифметическая, интерпретация * языка СРа состоит из

1) нормального недетерминированного предиката доказательств Pi и рекурсивных термов е(х, у), т(х,у), с(х), г(х) и п(х), удовлетворяющих операторным аксиомам;

2) оценки (•)*, сопоставляющей переменным по предложениям арифметические предложения, а переменным по доказательствам и аксиомным константам — замкнутые рекурсивные термы.

Оценка (•)* индуктивно продолжается на множество всех термов и формул языка CPQ:

7Smorynski С. Self-reference and modal logic. — New York, Berlin, Heidelberg, Tokio: Springer Verlag, 1985.

1) Т* = (0 = 0), 1* = (0 = 1) и * коммутирует с-булевыми связками; .

2) (t х а)' = m(i* ,*'), (« + *)• = e(l*. *•), (!«)' = c(fi'l), (Г tУ = г(Г), (ta t)* = п(Г);

3) (MF)* = Prf(t\ (OFy = Pr(f^l). •

1ите1)претация * удовлетворяет AS, если PA H Л* для всех формул L е AS.

Доказана корректность систем MCP as и М£Рд3 относительно писанной интерпретации:

[емма 1.17. Для любой AS -интерпретации *

1) MCP as Ь F =ф> PA Ь F*.

2) MCP as Ь F F* истинна в стандартной модели.

В § 1.3 определена семантика Крипке для систем, сформулирован-ых в § 1.1, и доказана соответствующая теорема о полноте.

Определение. Модель Крипке — это GL-модель К. = (К, -<, }=), которой отношение вынуждення удовлетворяет условиям стабиль-эстн (если а (¿J.4, с а и а -< Ь, то Ь }= |г]Л и с (= ¡[¿]Л) и рефлексивности (если а f= {¿J.4, то а {= Л), а также операторным ссномам. Если в модели /С выполняется аксномная спецификация S, то /С называется Л5-моделью.

еорема 1.20. (Корректность.)

ICVas Ь А =>■ Л истинна во всех AS-моделлх.

Поскольку доказательство арифметической полноты MCP as iic~ >льэует погружение моделей Крипке в формальную арифметику, юрема о полноте сформулирована относительно более узкого класса )долей, в которых отношение вынуждення в известной степени эф-иктивно.

пределение. Модель К. называется конечно-порожденной, если С, -() — конечное иррефлекенвное дерево, и множество всех ис-1нных (/-атомарных формул порождается из некоторого конечного южества при помощи бесконечной итерации правил операторного толчения, считанных с операторных аксиом.

Отношение вынуждення в таких моделях является эффектпвнь в следующем смысле: для всякого терма t множество

щ = {G I к: |= [*]<?}

конечно, и функция, сопоставляющая каждому терму t код мноа ства I(t), примитивно-рекурсивна.

Теорема 1.23. Если А истинна ао всех конечно-порожденных Л моделях, то МСР,\ц Ь А.

Для систем MCPUAS установлен аналогичный результат. Пус Г — произвольное множества формул. Модель Крипке AJ назыв ется Г-правильной, если ее корне истинна формула Н(Г) = A{Qß В\ПВ 6 5иЬ(Г)}. Тогда MCPJAS Ь .4 А истинна в корне люб(

конечно-порожденной {Л, Л5}~правильнои модели.

Из теоремы о модальной полноте непосредственно следует разр шимость логик MCPt\s ii MCPUAS.

В § 1.4 приведено доказательство теоремы об арнфметпческ< полноте систем MCPAs и MCP^AS.

Теорема 1.35.

1) MCPas (/ => PA I/ Л* для некоторой AS - интерпретации

2) MCPUAS I/ А А* ложна в стандартной модели для некот рой AS -интерпретации *.

Это доказательство объединяет стандартную конструкцию С ловея, примененную при доказательстве арифметической полнот GL, и построение подходящего предиката доказательств при номой арифметической теоремы о неподвижной точке, аналогичное [5].

В § 1.5 изучается вопрос о функциональной полноте MCP. Д казано, что функции х, +, !, ffa и образуют базис множест; операций над доказательствами, допускающих описание в модал ном пропозициональном языке. Этот факт объясняет выбор базов* операций для MCP.

Определение. Абстрактной пропозициональной операцией над с казательствими будем называть истинную в любой арнфметич ской интерпретации формулу вида С DG, где С — {V, А}-комб нация </-атомарных формул.

По сравнению с аналогичным определением из [5], мы допускаем ¡хождения .□ и функциональных символов в формулы С и G. Все опе-)ацин языка СРр могут быть представлены как абстрактные пропо-шцнональные операции над доказательствами. В частности, функ-щн |)-а и fta ]>еализуют соответственно операции

[х]см -> ал н [:t|.4 -> асы.

Теорема 1.45. Для всякой пропозициональной операции над дока-ательстпвами С —> OG найдется CVa-тсрм t и аксиомная спецификация AS, такие что

MCP ¿s ЬС-) MG.

В главе 2 изучается свойство Крейга для логик доказательств. По-кольку язык логик доказательств содержит переменные двух сор-ов, можно определить два варианта интерполяционного свойства. >бозначнм через ScntVur(Ä) и ProofVar(A) соответственно множе-гва переменных по предложениям и по доказательствам, входящих формулу А, и Var(A) = ProofVar(A) U SentVar{A).

)пределение. Логика С обладает слабым свойством Крейга, если ля всякой формулы А -> В, выводимой в С, найдется формула ф, азываемая слабым иптерполяптом для Л —* В, такая что С Ь (Л —» ) А (ф -> В) и SentVar{ф) С SentVar{A) П SentVar(B). Если же ыполняется условие Уаг(ф) С Var^4)n Var(B), то формула ф назы-1ется сильным иптерполяптом для Л —ъ В, и С обладает сильным ioücniüOM Крейга.

В § 2.1 рассматриваются логики доказательств с оператором до-шуемости. Это логики доказательств без операций, введенные в ], и система MCP., построенная в главе 1. Показано, что логика " обладает сильным интерполяционным свойством, в то время как хже слабое интерполяционное свойство не выполняется для осталь-ах систем (В, f, М, ?и,Ми и MCP).

В § 2.2 изучается интерполяционное свойство для динамической >гнкн доказательств СР. Доказано, что для минимальной логики р0, отвечающей пустой аксиомнои спецификации, выполняется слали и не выполняется сильный вариант интерполяционного свойства.

Также приведен пример, показывающий, что в случае AS ф 0 даж слабый вариант интерполяционного свойства, как правило, не выпох няется.

Глава 3 посвящена предикатному варианту динамической логик доказательств. Предикатные логики доказуемости были изучены работах [8], [10] и [9]. В [8] С. Н. Артемовым была установлена не арифметичность, следовательно ц неаксиоматнзируемость, логик QLT, описывающей все арифметически истинные законы формал! нон доказуемости. В [9] было показано, что логика QLT являете П1(ТА)-полной (где ТА — множество арифметических формул, не тинных в стандартной модели). Логика доказуемости, ограничен нал средствами РА, была изучена В. А. Варданяном: в [10] был доказано, что она является полной в классе П§ арифметической не рархии. Таким образом, вопрос о наличии эффективного опасани свойств доказуемости в предикатном языке был решен отрнцательне В главе 3 аналогичные нижние оценки сложности получены для ripe дикатных логик доказательств.

В § 3.1 даны основные определения. Рассматривается язык прс днкатов первого порядка (без равенства и функциональных симос лов), к которому добавлен счетный набор переменных по доказатпел1 ставам pa,pi,p2 • • • » оператор доказательств [•](•)• Формулы опреде ляются стандартным образом с дополнительным правилом: если j — е})ормула и р — - переменная по доказательствам, то F — фор мула с теми же свободными переменными, что и F.

Оценкой предикатного языка с оператором доказательств иазь вается произвольное отображение /, сопоставляющее всякой пере менной по доказательствам натуральное число, а каждой атомарно формуле — арифметическую формулу с тем же набором свободны

8Артемов C.IÏ. О логиках, имеющих доказуемостную пнтерпретг цию // Сложность вычислений ь прикладная математическая Л1 гика\ Вопросы кибернетики. — Москва, 1988. — С. 5-22.

9Boolos G., McGee V. The degree of the set of sentences of prédicat provability logic that are true under every interpretation // ./. of Symbol; Logic. — 1987. — Vol. 52, N 2. — P. 165-171.

шВарданян В.А. Оценки арифметической сложности предикатны логик доказуемости // Сложность вычислений и прикладная мапи матическая логика: Вопросы кибернетики. — Москва, 1988. — С 46-72.

[временных. Считаем, что / коммутирует с операцией замены сво-одных переменных. Всякая пара * = (Л/>/)» где Pif — стандарт-;ый предикат доказательств, и / — оценка, задает интерпретацию юрмул этого языка следующим образом:

1) для атомарных формул Q* v^ fQ\

2) * коммутирует с булевыми связками и кванторами, то есть (Л V В)' ^ А* V В\ (УхЛ)* VxA* и т.д.;

3) (Ш(*и- ■ .,*»))* - Prf(JP, ГЛ*(А,,.. ..¿,,)1),

где f<£(ib .. ,,х„)] — естественный арифметический терм для примитивно-рекурсивной функции Axi...x„. [ф(х1,... ,х„)], которая по набору чисел ki,...,k„ вычисляет геделев номер формулы ф(к1,..., к„).

Арифметической теории U соответствует множество формул в редикатном языке с операторами доказательств, выводимых в U рн любом арифметическом переводе

QP£(U) т^ {Л | V* U h Л'}.

1ножество QPC(U) является логикой (т.е. содержит классическое счисление предикатов и замкнуто относительно стандартных пра-ил вывода) и оппсывает те свойства предикатов доказательств, ко-орые можно обосновать средствами теории U. В качестве U рас-матрнваются арифметика Пеано РА и истинностная арифметика А.. Соответствующие логики обозначаются QV и TQV.

В § 3.2 получено утверждение о неарнфметичности истинностной эгнкп доказательств TQP.

"еорема 3.3. Множество TQV не является арифметическим.

Доказательство использует метод, аналогичный [8]. С помощью инструкции из [9], можно показать, что TQP является Tlj(TA)-олной.

В § 3.3 изучается сложность логики QP.

>пределение. Арифметическая формула А(х) разрешима в теории если для всякий константы п £ и и U выводима одна из формул (/¡) пли Множества вида {n|{7 h Л(н)}, где формула Л

азрешпма в U, называются разрешимыми в теории U. Множество

принадлежит классу П„ (£„) u U, если оно имеет сложность П„ (Е относительно некоторого множества, разрешимого в U.

Теорема 3.9. Пусть U — непротиворечивая арифметическая те рия. Тогда имеет место т-сводимость любого множества из кла1 П2 в U к QP£(U).

Следствие 3.10. Всякое множество из П® может быть сведено QV, а значит логика QP не является перечислимой.

Благодарности. Пользуясь случаем, автор выражает глубоку благодарность научному руководителю профессору С. Н. Артемов за постановку задачи и неоценимую помощь на всех этапах работь а также к.ф.-м.н. Л. Д. Беклемишеву и доценту В. Н. Крупскому з плодотворные обсуждения и ценные советы.

РАБОТЫ ПО ТЕМЕ ДИССЕРТАЦИИ

1) Sidon T.L. Craig interpolation property in modal logics with pro\ ability interpretations // Lect. Notes in Сотр. Sci. — 199-1. — Vo 813. — P. 329 340.

2) Sidon T.L. On interpolation property for modal provability logics / 10th international congress of logic, methodology and philosophy с science. Volume of abstracts. — 1995. — P. G2.

3) Sidon T.L. Provability logic with operations on proofs // Lect. Note in Сотр. Sci. — 1997. — Vol. 1234. — P. 342-353.

4) Сидон Т. Л. Логика доказуемости с операциями над доказа тельствамн // Фундаментальная и прикладная математика. — 1997. — Т. 3, вып. 4. — С. 1173-1197.