Выразительные возможности оператора частичной неподвижной точки для конечных и бесконечных систем тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Секорин Всеслав Станиславович

• Секорин Всеслав Станиславович
• кандидат наук
• 2024

Оглавление диссертации кандидат наук Секорин Всеслав Станиславович

Обзор литературы

Цель работы

Методы исследования

Положения, выносимые на защиту, и научная новизна

Апробация работы

Публикации

Структура работы

1 Основные определения

1.1 Классическая логика

1.2 Определение РЕР-оператора для конечных алгебраических систем

1.3 Определение РЕР-оператора для бесконечных алгебраических систем

2 О соотношении выразительных возможностей различных семантик РЕР-оператора

V/ ^

2.1 Об эквивалентности РЕР и РЕР операторов

2.2 Об эквивалентности оператора частичной неподвижной точки и квантора

2.3 Об элиминации оператора частичной неподвижной точки в

счётно-категоричной теории

3 Логика второго порядка и РЕР-оператор для конечных систем

3.1 Вспомогательные построения

3.2 Булевы операции

3.3 Вложенные РЕР-операторы

3.4 Алгоритм устранения РЕР-оператора при наличии линейного порядка

4 Сравнение выразительных возможностей 1ЕР и РЕР операторов

4.1 Определение инфляционной неподвижной точки

4.2 Об определении бесконечного дискретного предпорядка

4.3 Моделирование РЕР-оператора

5 О неразрешимости логики с РЕР-оператором

5.1 Определение машины Минского

5.2 Моделирование машины Минского

5.3 Теория следования с первым элементом

Заключение

Литература

Введение

Введение диссертации (часть автореферата) на тему «Выразительные возможности оператора частичной неподвижной точки для конечных и бесконечных систем»

Актуальность работы

Изучение выразительных возможностей различных формальных языков является одной из основных задач математической логики. Оно включает в себя исследование структуры формальных языков, соотношений между формальными языками, сравнение выразительных возможностей разных формальных языков, взаимосвязи синтаксиса и семантики языков, различных алгоритмических проблем, которые возникают при работе с формальными языками и многие другие вопросы. Изучение теоретических проблем в этой области становится все более актуальным и важным, а также приобретает практическую значимость в современном мире, где информационные технологии получают всё более широкое распространение, поскольку различные методы и средства математической логики находят разнообразные и многочисленные применения при проектировании и анализе программного обеспечения.

Теория логических языков является тем разделом математической логики, который наиболее тесно связан с информатикой. Данные языки широко используются, например, в различных системах управления базами данных, где они служат в качестве средства для извлечения информации, а также средством декларативного описания целостности данных. Типичной и одной из самых распространённых на данный момент моделью базы данных является реляционная модель, которая была предложена Э. Код-дом в работах [21] и [22]. В данной модели база данных представляется

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

В качестве языка извлечения данных Э. Коддом было предложено реляционное исчисление, которое эквивалентно языку логики предикатов. Но в статье [16] Ахо А. и Ульман Д. отметили, что этот язык обладает довольно ограниченной выразительной силой: в нём нельзя выразить транзитивное замыкание произвольного графа. Ещё одним классическим примером, который невозможно выразить с помощью языка логики первого порядка, является определение чётности количества элементов в конечном линейном порядке, когда сигнатура не содержит других отношений и функций.

Логика второго порядка гораздо более выразительна. Из [33] известно, что для конечных алгебраических систем она соответствует объединению полиномиальной иерархии РН. Но с практической точки зрения язык логики второго порядка имеет существенный недостаток: отсутствует явный способ нахождения предикатов, находящихся под кванторами.

Существуют другие расширения логики первого порядка, которые лишены этого недостатка. Уже в статье [16] Ахо А. и Ульман Д. предложили расширить логику первого порядка добавлением итеративных операторов. В самой этой работе в качестве такого оператора предлагался оператор наименьшей неподвижной точки (ЬРР), который, в частности, позволяет определить транзитивное замыкание любого графа. Он же решает и проблему определения чётности для конечного линейного порядка.

Другими примерами итеративных операторов являются оператор транзитивного замыкания (ТС), оператор инфляционной неподвижной точки

(1ЕР) и оператор частичной неподвижной точки (РЕР). Все перечисленные операторы, очевидно, лишены того недостатка, который мы выше указали для логики второго порядка, так как способ нахождения значения явно задан в их определении. Отметим, что многие современные системы управления базами данных используют языки построения запросов, содержащие конструкции эквивалентные каким-то из указанных выше итеративных операторов, чаще всего — операторам неподвижной точки. Находят эти операторы и другие применения, например, при описании тех или иных процессов, развивающихся во времени [18, 19]. Таким образом, изучение свойств различных операторов неподвижной точки является важным и с теоретической, и с практической точек зрения. Значительная часть современных работ по математической логике как раз посвящена исследованиям обогащений такими операторами различных классических и неклассических логических языков [17, 23, 26, 30].

Самым универсальным из перечисленных итеративных операторов является оператор частичной неподвижной точки, так как он позволяет определить другие операторы. Впервые понятие частичной неподвижной точки вводится в статье [27] и даётся его описание. Книга [32] содержит многие классические результаты: определения синтаксиса и семантики оператора частичной неподвижной точки для конечных алгебраических систем, доказывается, что при наличии линейного порядка логика этого оператора соответствует классу РБРАСЕ. Кроме того, рассматриваются свойства языка запросов к базам данных, обогащённого оператором неподвижной точки.

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

является более сложной: разные определения, которые эквивалентны для конечных систем, будут иметь разную семантику для бесконечных. Этот вопрос был затронут в работе [31]. В ней рассматривается одна из семантик оператора частичной неподвижной точки, которая определяется трансфинитной индукцией по произвольным ординалам. Если ограничиться только натуральными числами, то результат РЕР-оператора в этой семантике содержит в точности те наборы, которые входят в почти все построенные предикаты (то есть все, начиная с некоторого). Таким образом, это определение как раз является примером обобщения семантики РЕР-оператора с конечных систем на бесконечные. В той же работе доказано, что для произвольных систем РЕР-оператор рассматриваемой семантики является строго более выразительным, чем оператор инфляционной неподвижной точки.

Важно заметить, что обогащения итеративными операторами могут значительно повлиять на различные свойства теории, например, сделать её неразрешимой [31]. С другой стороны, обогащение необязательно увеличит выразительные возможности, например, существование в-функции Гёде-ля в арифметике позволяет промоделировать некоторые семантики неподвижной точки уже в языке логики первого порядка и без специального оператора.

С алгоритмической точки зрения одним из важнейших свойств операторов неподвижной точки является возможность вычисления за конечное число шагов, именно такие варианты итеративных операторов представляют практическую ценность. Данное свойство называется сходимостью, и для оператора инфляционной неподвижной точки было изучено в работах Дудакова С.М. [24, 25].

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

Обзор литературы

Основополагающие идеи о представлении базы данных с помощью реляционной модели, которые в конце концов и возбудили интерес к расширению языка математической логики итерационными операторами, были высказаны Э. Коддом в работах [21] и [22], где была впервые предложена концепция реляционной базы данных. Одни из первых исследований языка реляционной алгебры — это работы [16] и [19] А. Ахо, Дж. Ульмана, А. Чан-дры и Д. Харрела. В них продемонстрировано, что реляционная алгебра, как язык извлечения данных, эквивалентна по выразительной силе языку логики первого порядка. Там же указаны и первые примеры свойств конечных алгебраических систем, которые с помощью логики первого порядка не выражаются.

Сама идея итеративного оператора — оператора наименьшей неподвижной точки — также высказана в [16]. Идея частичной неподвижной точки, как более общего варианта итеративного оператора для конечных алгебраических систем, предложена Ю. Гуревичем в [27]. С самого начала возникла идея отождествления выразительной силы языков, получаемых добавлением тех или иных операторов, с соответствующими проблемами в теории алгоритмов, в частности, сложностными классами. Ряд работ, например, [28, 29] как раз посвящены этим проблемам. Книга Л. Либкина [32] содержит подробный материал о перечисленных выше языках, включая языки неподвижных точек и язык логики второго порядка, для конечных систем, а также о результатах об их выразительных возможностях.

Перенос итеративных операторов с конечных систем на бесконечные может порождать проблемы с разными определениями, что, например, продемонстрировано С. Кройцером в [31]. Очень часто для бесконечных систем построение результата итеративного оператора представляет собой алгоритмически неразрешимую задачу даже для достаточно простых теорий.

Скажем А. С. Золотов в [34] показал, что логика унарного транзитивного замыкания неразрешима для аддитивной теории натуральных чисел. В связи с этим исследованы некоторые ситуации, в которых удаётся иногда увеличить выразительные возможности языка первого порядка, не расширяя сам язык, а расширяя вместо этого универсум, и сохранив при этом алгоритмическую разрешимость. Некоторые из таких примеров приведены в работе М. А. Тайцлина и С.М. Дудакова [12]. Но описанное увеличение выразительной силы крайне специфично и малополезно в реальных ситуациях.

Тем не менее известен ряд случаев, когда алгоритмические проблемы, связанные с итеративными операторами, оказываются разрешимыми. Например, в статье А. С. Золотова [13] указан явный алгоритм, который по формуле с оператором транзитивного замыкания по одной паре переменных в теории следования позволяет эффективно избавиться от этого оператора. Ситуации, когда результат оператора инфляционной неподвижной точки получается за конечное число шагов, что в ряде случаев приводит к алгоритмической разрешимости рассмотрены в работах С. М. Дудако-ва [10] и [24]. Там же показано, что за счёт увеличения местности можно элиминировать все 1РР-операторы, кроме одного. Поскольку после этого 1РР-оператор применяется к формуле первого порядка, то появляется возможность связать свойства 1РР-языка со свойствами языка первого порядка, например, категоричностью теорий. Увеличение местности операторов при этом существенно, так как в [25] установлено, что, например, оставаясь в рамках только унарных операторов этого сделать нельзя: выразительные и алгоритмические свойства унарных и бинарных операторов могут быть существенно различны.

Цель работы

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

В работе решаются следующие задачи:

1) Изучение различных вариантов семантик оператора частичной неподвижной точки. Исследование соотношения выразительных возможностей логики первого порядка, обогащённой различными операторами частичной неподвижной точки.

2) Исследование соотношения выразительных возможностей логики первого порядка, обогащённой оператором частичной неподвижной точки, и логики второго порядка, обогащённой этим оператором, для конечных алгебраических систем.

3) Исследование возможности элиминации оператора частичной неподвижной точки при различных условиях.

4) Исследование алгоритмической разрешимости логики оператора частичной неподвижной точки для функции следования.

Методы исследования

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

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

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

3) Разработан метод моделирования машины Минского при помощи формул логики первого порядка, которая обогащена оператором частичной неподвижной точки.

Положения, выносимые на защиту, и научная новизна

Все результаты, которые получены в данной работе, являются новыми.

На защиту выносятся следующие результаты:

1) Показано, что расширения логики первого порядка операторами РРРУ, РРР3 и РРР-квантор для оператора частичной неподвижной точки для бесконечных алгебраических систем дают эквивалентные между собой по выразительным возможностям логические языки.

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

3) Показано, что в конечных алгебраических системах с линейным порядком всякая формула логики второго порядка, обогащённой оператором частичной неподвижной точки, эквивалентна формуле логики первого порядка с всего одним вхождением оператора частичной неподвижной точки. Кроме того, показана возможность элиминации РРР-оператора в счётно-категоричной теории.

4) Показано, что проблема истинности формулы, содержащей оператор частичной неподвижной точки, является неразрешимой для теорий целых и натуральных чисел с функцией следования. Это выполнено и в случае, когда оператор является унарным, невложенным и единственным.

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

Апробация работы

Результаты и положения диссертации докладывались и обсуждались на следующих конференциях и семинарах:

1) Международная научная конференция «Алгебра и математическая логика: теория и приложения» (Казань, Казанский (Приволжский) федеральный университет, 2019).

2) Международная конференция «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж, Воронежский государственный университет, 2019).

3) Семинары «Теоретические основы информатики» (Тверь, Тверской государственный университет, 2019-2022).

4) Международная конференция «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж, Воронежский государственный университет, 2020).

5) Всероссийская научная конференция «Математические основы информатики и информационно-коммуникационных систем» (Тверь, Тверской государственный университет, 2021).

Публикации

Автор имеет 8 опубликованных работ, в том числе по теме диссертации 7. Из них одна статья [6] опубликована в рецензируемом научном издании, индексируемом в базах данных Scopus и Web of Science. Одна из статей [7] — в рецензируемом научном издании, индексируемом в Scopus. Две статьи [1], [3] опубликованы в рецензируемом научном издании, входящем в перечень ВАК. Остальные работы опубликованы в списке трудов различных международных и всероссийских конференций. Список публикаций приведён в конце работы.

В работе [1] приведены определения семантик PFPV и PFP3 для оператора частичной неподвижной точки для бесконечной алгебраической системы. Также для них доказывается равенство выразительных возможностей. В статье [2] доказывается, что оператор частичной неподвижной точки в теории одного следования является неразрешимой. В статье [3] показано, что оператор частичной неподвижной точки можно промоделировать оператором инфляционной неподвижной точки в алгебраических системах, содержащих строгий частичный порядок со сколь угодно длинными цепями. В работах [4, 7] доказывается, что логики, обогащенные PFP-оператором и PFP-квантором, обладают равными выразительными возможностями. Статья [5] содержит доказательство того, что для произвольной формулы логики второго порядка с несколькими PFP-операторами можно построить эквивалентную формулу логики первого порядка с только одним PFP-оператором. В статье [6] приводится алгоритм, при помощи которого формулу логики первого или второго порядка с несколькими операторами

частичной неподвижной точки, можно привести к формуле логики первого порядка лишь с одним оператором частичной неподвижной точки.

Структура работы

Диссертация состоит из введения, шести глав, заключения и списка использованной литературы. Полный объём работы — 111 страниц, список литературы содержит 34 наименования.

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

В первой главе даны определения для классической логики и логики оператора частичной неподвижной точки. В параграфе 1.1 даются определения терма, атомарной формулы, формулы, значения терма и значения формулы для логики первого порядка. После определяем аналогичные понятия для логики второго порядка. Так же приводятся примеры ко всем основным определениям. В параграфе 1.2 даются определения формулы РРР-логики и её значения для конечных алгебраических систем. Приводится пример оператора частичной неподвижной точки, описывается принцип её построения и определяется значение. В параграфе 1.3 даются несколько различных определений семантике формуле в логике частичной неподвижной точки и приводятся примеры их использования.

Во второй главе рассматривается соотношение выразительных возможностей различных семантик оператора частичной неподвижной точки, та-

V/ ^ V/

ких как РРР -оператор, РРР -оператор и РРР -квантор, для бесконечных алгебраических систем. Вторым рассматриваемым вопросом является возможность элиминации оператора неподвижной точки для бесконечных алгебраических систем в счётно-категоричных теориях. В параграфе 2.1 доказывается равенство выразительных возможностей для семантик

V/ ^

РРР -оператора и РРР -оператора. В параграфе 2.2 доказывается равен-

у7

ство выразительных возможностей для семантик РРР -оператора и РРР-квантора. В последнем параграфе 2.3 доказываем теорему о том, что в счётно-категоричной теории РРР -оператор можно элиминировать.

В третьей главе рассматривается оператор частичной неподвижной точки для логики второго порядка и конечной алгебраической системы. Основным результатом является то, что в конечной системе мы можем для произвольной формулы логики первого порядка с несколькими операторами частичной неподвижной точки построить эквивалентную формулу логики первого порядка с только одним РРР-оператором. Аналогично для логики второго мы демонстрируем, как для формулы с несколькими РРР-операторами построить эквивалентную формулу логики первого порядка с только одним РРР-оператором. Параграф 3.1 содержит используемые в работе обозначения, и в нём даётся их описание. В параграфе 3.2 показывается, как преобразовать конъюнкцию оператора РРР с некоторой формулой или отрицание РРР-оператора к новому оператору частичной неподвижной точки. Далее доказывается корректность таких преобразований, для этого показывается корректность вспомогательных лемм, содержащих утверждения о том какие значения принимает новый оператор РРР во время построения. В параграфе 3.3 показывается, как можно преобразовать формулу со вложенными операторами РРР к формуле с одним оператором частичной неподвижной точки. Для того чтобы показать корректность данных изменений, доказывается две дополнительные леммы: о значении нового оператора РРР на каждом шаге построения, и о конечности и максимальном количестве шагов построения нового оператора РРР, выполняемых для определения значения внутреннего оператора РРР. Параграф 3.4 содержит теорему, показывающую как к любой формуле можно добавить фиктивный оператор частичной неподвижной точки, и доказательство корректности данного преобразования. Используя это мы доказываем теорему, в которой приводим алгоритм, как по любой формуле

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

В четвёртой главе рассматривается соотношение выразительных возможностей операторов частичной и инфляционной неподвижной точки в бесконечных алгебраических системах, содержащих отношение строгого частичного порядка. В параграфе 4.2 при помощи формулы с оператором инфляционной неподвижной точки мы зададим нестрогий предпоря-док. Для него доказываем лемму, что определённая нами формула задаёт нестрогий предпорядок на множестве пар. Далее мы покажем, что этот предпорядок является дискретным и в нём имеется бесконечная дискретная цепь подряд идущих элементов. В параграфе 4.3 мы показываем, как для семантик РРР, РРР и РРР оператора частичной неподвижной точки построить эквивалентную формулу, содержащую 1РР-оператор, но не содержащую РРР-оператор. Для каждой семантики мы формулируем и доказываем вспомогательную лемму, говорящую о соотношении шагов построения операторов инфляционной и частичной неподвижной точки. После доказываем основные теоремы, показывающие корректность построенных нами формул.

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

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

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

Глава 1

Основные определения

1.1 Классическая логика

Для начала определим синтаксис логики первого порядка. Для этого последовательно приведём определения таких понятий как терм, атомарная формула и формула.

Определение 1 (Терм, см. [8]). Термом называется последовательность, которая состоит из переменных, функциональных символов, скобок и запятых, и строится по следующим правилам:

• переменная является термом,

• функциональный символ нулевой местности (называемый константой) является термом,

• /(¿1,... ,£п) является термом, если ..., ¿п — термы и / — функциональный символ местности п.

Используя понятие терма, дадим следующие определения, начиная с атомарной формулы.

Определение 2 (Атомарная формула, см. [8]). Атомарной формулой является следующее:

• предикатный символ нулевой местности,

• выражение Р(¿1,..., Ьп), где Р — предикатный символ местности п,

,..., ¿п — термы,

• выражение = где и — термы.

Теперь можно дать определение формулы логики первого порядка.

Определение 3 (Формула логики первого порядка, см. [8]). Формулой логики первого порядка называется слово, построенное по следующим правилам:

• атомарная формула — формула,

• если ф — формула, то —ф — формула,

• если ф и ф — формулы, то ф Л гф, ф V ф и ф ^ ф также являются формулами,

• если ф — формула, х — переменная, то (Зх)ф и (Vх)ф являются формулами.

Приведём пример формулы логики первого порядка.

Пример 1. Запишем одну из аксиом теории дискретного линейного порядка:

(Vx) ^(Зу)х < у ^ (Зу)(х < у Л (Vz)(х < г ^ у < х))^.

Замечание 1. В дальнейшем в формулах могут содержаться скобки, отличные от круглых, они призваны сделать формулы более читабельными.

После определений синтаксиса можно перейти к определению семантики формул логики первого порядка. Для начала приведём определение состояния в алгебраической системе и значений терма и атомарной формулы.

Определение 4 (Алгебраическая система и состояние, см. [11]). Алгебраической системой А сигнатуры 2 называется пара (А, и), где А (носитель) — произвольное непустое множество, а V — интерпретирующая функция, которая ставит в соответствии каждому сигнатурному символу функцию или предикат.

Под состоянием а некоторой алгебраической системы А = (А, V) понимается отображение множества переменных V в А.

Если а € |А|, то при помощи (а)Х мы обозначаем состояние т, для которого т (х) = а и т (у) = а (у) для всех остальных переменных у.

Список литературы диссертационного исследования кандидат наук Секорин Всеслав Станиславович, 2024 год

Литература

Публикации автора по теме диссертации.

[1] Секорин В. С. Об эквивалентности двух семантик РРР-оператора // Вестник Тверского государственного университета. Серия: Прикладная математика. — 2020. — N0.3. — С. 41-49.

[2] Секорин В. С. Неразрешимость одноместных РРР-операторов без вложения в теории одного следования // Актуальные проблемы прикладной математики, информатики и механики: Сборник трудов Международной научной конференции, Воронеж, 13-15 декабря 2021 года. — Воронеж: Общество с ограниченной ответственностью «Вэл-борн», 2022. — С. 1665-1670.

[3] Секорин В. С. Моделирование оператора частичной фиксированной точки. // Вестник Тверского государственного университета. Серия: Прикладная математика. — 2022. — N0. 2. — С. 14-26.

[4] Секорин В. С. Об эквивалентности РРР-оператора и РРР-квантора // Актуальные проблемы прикладной математики, информатики и механики: сборник трудов Международной научной конференции, Воронеж, 07-09 декабря 2020 года / ФГБОУ ВО «Воронежский государственный университет». — Воронеж: Научно-исследовательские публикации, 2021. — С. 1628-1635.

[5] Секорин В. С. Элиминация оператора частичной фиксированной точки // Всероссийская научная конференция «Математические основы

информатики и информационно-коммуникационных систем»: сборник трудов. Всероссийская научная конференция, Тверь, 03-08 декабря 2021 года. — Тверь: Тверской государственный университет, 2021. — С.255-261.

[6] Sekorin V. S. Partial Fixed Point for Finite Models in Second Order Logic // Lobachevskii Journal of Mathematics. — 2020. — Vol.41, No. 9. — P. 1672-1679.

[7] Sekorin V. S. On Equivalence of PFP-operator and PFP-quantifier // Journal of Physics: Conference Series: Current Problems, Voronezh, 07-09 December 2020. — 2021. — Vol 1902. — P. 012085. — DOI 10.1088/17426596/1902/1/012085.

Использованная литература.

[8] Верещагин Н.К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. 4-е изд., испр. — М.: Издательство МЦНМО, 2012. — 240 c.

[9] Голдблатт Р. Топосы. Категорный анализ логики. — М.: Мир, 2020. — 488 с.

[10] Дудаков С. М. О безопасности рекурсивных запросов // Вестник ТвГУ. Серия: Прикладная математика. — 2012. — No. 4. — С. 71-80.

[11] Дудаков С. М. Основы теории моделей: Учебник. — Тверь: Твер. гос. ун-т, 2013. — 480 с.

[12] Дудаков С.М., Тайцлин М.А. Трансляционные результаты для языков запросов в теории баз данных // Успехи математических наук. — 2006. — Т. 61, No. 2(368). — С. 2-65.

[13] Золотов А. С. Об элиминации оператора фиксированной точки для некоторых формул в теории одного следования // Вестник ТвГУ. Серия: Прикладная математика. — 2015. — No. 4. — С. 27-37.

[14] Мальцев А. И. Алгебраические системы. — М.: Наука, 1970. — 392 c.

[15] Минский М. Вычисления и автоматы. — М.: Мир, 1971. — 366 с.

[16] Aho A., Ullman J. The universality of data retrieval languages. // Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. — New York: Association for Computing Machinery, 1979. — P. 110-120.

[17] Berger U., Tsuiki H. Intuitionistic fixed point logic // Annals of Pure and Applied Logic — 2021. — Vol. 172, No. 3. — P. 102903.

[18] Bodirsky M., Pakusa W., Rydval J. Temporal Constraint Satisfaction Problems in Fixed-Point Logic // Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. — New York: Association for Computing Machinery, 2020. — P. 237-251.

[19] Chandra A., Harel D. Computable queries for relational databases // Journal of Computer and System Sciences. — 1980. — Vol.21, issue2. — P. 156-178.

[20] Chandlee J., Jardine A. Quantifier-free least fixed point functions for phonology // Conference: Proceedings of the 16th Meeting on the Mathematics of Language. — Toronto: Association for Computational Linguistics, 2019. — P. 50-62.

[21] Codd E. F. A relational model for large shared data banks. // Communications of the ACM. — 1970. — Vol. 13. — P. 377-387.

[22] Codd E. F. Relational completeness of data base sublanguages. // Database Systems (ed. Rustin R.) — Prentice Hall and IBM Research Report. — 1972. — Vol. RJ987. — P. 33-64.

[23] Dannert K.M., Graedel E., Naaf M., Tannen V. Semiring Provenance for Fixed-Point Logic // 29th EACSL Annual Conference on Computer Science Logic. — Wadern: Dagstuhl Publishing, 2021. — P. 17:1-17:22.

[24] Dudakov S.M. On Inflationary Fix-Point Operators Safety. // Lobachevskii Journal of Mathematics. — 2015. — Vol. 36, No. 4. — P. 328331.

[25] Dudakov S.M. On Safety of Unary and Nonunary IFP Operators // Automatic Control and Computer Sciences. — 2019. — Vol. 53, No. 7. — P. 683-688.

[26] Graedel E., Grohe M., Pago B., Pakusa W. A Finite-Model-Theoretic view on propositional proof complexity // Logical Methods in Computer Science. — 2019. — Vol. 15, issue 1. — P. 4:1-4:55.

[27] Gurevich Y., Shelah S. Fixed-point extensions of first-order logic. // Annals of Pure and Applied Logic. — 1986. — Vol. 32. — P. 265-280.

[28] Gurevich Y. Toward logic tailored for computational complexity. // Computation and Proof Theory. Lecture Notes in Mathematics 1104. — Berlin: Springer, 1984. — P. 175-216.

[29] Immerman N. Languages That Capture Complexity Classes // SIAM Journal of Computing. — 1987. — Vol. 16. — P. 760-778.

[30] Jaeger G. Short note: Least fixed points versus least closed points // Archive for Mathematical Logic. — 2021. — Vol. 60. — P. 831-835.

[31] Kreutzer S. Partial Fixed-Point Logic on Infinite Structure // Computer Science Logic. Lecture Notes in Computer Science 2471. — Berlin: Springer, 2002. — P. 337-351.

[32] Libkin L. Elements of Finite Model Theory. — Berlin: Springer, 2012. — 314p.

[33] Stockmeyer L. The polynomial-time hierarchy // Theoretical Computer Science. — 1977. — Vol. 3. — P. 1-22.

[34] Zolotov A. S. On decidability of the theory with the transitive closure operator. // Lobachevskii Journal of Mathematics. — 2015. — Vol. 36, No. 4. — P. 434-440.