Алгоритмические и семантические вопросы математической логики. 2016-2020НИР

Algorithmic and semantic problems of mathematical logic. 2016-2020

Источник финансирования НИР

госбюджет, раздел 0110 (для тем по госзаданию)

Этапы НИР

# Сроки Название
1 1 января 2016 г.-31 декабря 2016 г. Алгоритмические и семантические вопросы математической логики. 2016
Результаты этапа: Алгоритмическая статистика для алгоритмов с ограничением времени работы: найдено годное определение стохастичности и доказано существование нестохастических объектов. Получена точная оценка сложности интуиционистской эпистемической логики IEL. Введена конструктивная семантика для языка теории множеств с атомами и исследован вопрос о корректности различных аксиом классической теории множеств относительно этой семантики. Доказано, что определимые тонкие борелевские множества (в частности, цепи) кофинальны; построена модель, в которой П1,2-множества со счётными сечениями не униформизуемы. Построен линейной сложности алгоритм кратчайшей перестройки графов при разных ценах операций. Построены кубической сложности модели эволюции видов и регуляции клеточных процессов. Доказана алгоритмическая неразрешимость нескольких вариантов исчисления Ламбека с субэкспоненциальными модальностями, одна из которых допускает правило нелокального сокращения. Разработано расширение некоммутативной линейной логики с несколькими взаимозависимыми субэкспоненциальными модальностями, доказана теорема об устранении сечения. Доказана П_2^0-трудность для исчисления Ламбека с экспоненциальной модальностью и "звёздочкой Клини".
2 1 января 2017 г.-31 декабря 2017 г. Алгоритмические и семантические вопросы математической логики. 2017
Результаты этапа: Доказано существование замощения всей плоскости, кроме некоторой ограниченной области, шестиугольниками Амманна, удовлетворяющее локальным правилам, для которого нет замощения всей плоскости, удовлетворяющего локальным правилам, которое совпадало бы с исходным везде, кроме некоторой ограниченной области (которая может быть больше, чем исходная незамощённая область). Разработана семантика реализуемости для конструктивной теории множеств, основанная на гиперарифметической вычислимости. Доказана эквивалентность конъюнктивных грамматик (по Охотину) и базовых категориальных грамматик, обогащённых операцией конъюнкции. Доказана сводимость линейным алгоритмом задачи преобразования графов к задаче целочисленного линейного программирования квадратичного размера. Построено определимое счётное множество, не содержащее определимых элементов. Все рассмотренные конкретные задачи решены в полном объёме.
3 1 января 2018 г.-31 декабря 2018 г. Алгоритмические и семантические вопросы математической логики. 2018
Результаты этапа: Изучалось понятие абстрактной логической системы, состоящей из языка (множества формул), класса структур (моделей) и отношения истинности между ними. Золиным получен критерий аксиоматизируемости произвольного класса структур: класс структур аксиоматизируем тогда и только тогда, когда он является компактным и замкнутым относительно эквивалентности моделей. Данный критерий получен при некоторых слабых естественных условиях, удовлетворяемых многими логическими системами, такими как логика предикатов; модальные логики с универсальной модальностью или модальностью неравенства; модальные и интуиционистские предикатные логики. Категориальные грамматики - это логико-математический формализм, используемый для описания синтаксиса естественных языков и построения автоматизированных синтаксических анализаторов. В одном из таких анализаторов, CatLog (разрабатывается группой специалистов в Барселоне), используются скобки (brackets) для уточнения синтаксического анализа: например, допуская конструкции вида "кошка, [которую Вася вчера видел]", система со скобками блокирует некорректные конструкции вида "мышь, [которую Вася вчера видел кошку, [которая поймала]]". Недостатком существовавшей версии CatLog была необходимость подавать скобочную структуру алгоритму на вход. Был разработан улучшенный алгоритм для CatLog, автоматически определяющий скобочную структуру и при этом работающий настолько же эффективно. (совместный результат С.Л. Кузнецова с Г. Морриллом, М.И. Кановичем и А. Щедровым)
4 1 января 2019 г.-31 декабря 2019 г. Алгоритмические и семантические вопросы математической логики. 2019
Результаты этапа: В области неклассических логик Доказана неарифметичность логики предикатов, основанной на понятии строго примитивно рекурсивной реализуемости. Это понятие было предложено З.Дамняновичем. Он же предложил доказательство утверждения о корректности интуиционистского исчисления предикатов относительно строго примитивно рекурсивной реализуемости. Опираясь на это утверждение Б.Х.Пак в 2003 году доказал неарифметичность рассматриваемой логики. Впоследствии В.Е.Плиско обнаружил пробел в доказательстве Дамняновича и построил контрпример к его утверждению. Теперь В.Е. Плиско получено доказательство теоремы Пака, не использующее указанного утверждения Дамняновича. Предложена полная аксиоматизация свойства точности модели логики свидетельств. Разработаны понятия модальной k-насыщенности и модальной k-компактности модели Крипке, соответствующие инфинитарным модальным языкам, в которых позволяется брать конъюнкцию множества формул, имеющего мощность менее k, где k - бесконечный регулярный кардинал. Доказано, что на моделях, являющихся одновременно k-насыщенными и k-компактными, отношение модальной эквивалентности (в указанном инфинитарном модальном языке) совпадает с отношением бисимуляции (структурным отношением, в котором не фигурирует модальный язык). Для произвольных модальных логик доказан аналог результата, полученного W. Dziobiak в 1980 г. для интуиционистской логики: непротиворечивая нормальная логика является сильно полной относительно класса всех своих конечных шкал Крипке тогда и только тогда, когда она является табличной, то есть является логикой некоторой конечной шкалы Крипке. Доказано, что операция взятия евклидова замыкания бинарного отношения является (как частный случай хорнова замыкания отношения) согласованной с минимальной фильтрацией, и согласованной с максимальной фильтрацией. Тем самым модальная логика евклидовых шкал Крипке (обозначаемая K5), а также модальная логика с двумя отношениями, одно из которых является евклидовым замыканием другого, допускают фильтрацию: всякую модель данной логики можно профакторизовать в конечную модель со шкалой данной логики (для самой логики K5 результат был ранее получен другими методами). В области теории определимости Получено полное описание инъективных отображений, сохраняющих отношения, производные от порядка (редукты порядка): «между», «цикл», «зацепление». Получено решение проблемы Элгота - Рабина, в классе структур включающих порядок натуральных чисел: доказано, что среди таких структур нет максимальной разрешимой. В области сложности вычислений Построено новое семейство апериодических замощений плоскости прямоугольными треугольниками, задаваемое локальными правилами. Ранее были известны два подобных семейства замощений: замощения Пенроуза равнобедренными треугольниками и т.н. Pinwheel tilings. Получено доказательство законов сохранения взаимной информации в бесконечных двоичных последовательностях относительно преобразований, выполняемых вероятностными алгоритмами (для определения Л. Левина 1974 года). В области теории исчислений и комбинаторики слов Найден эффективный критерий выводимости в исчислении Ламбека с одним делением, обогащённом субструктурной модальностью, допускающей правило ослабления. Доказана алгоритмическая неразрешимость и сигма-1 полнота проблемы выводимости для исчисления Ламбека с аддитивными операциями и итерацией Клини, аксиоматизированной принципом «чистой индукции» Пратта (проблема поставлена у Д. Козена в 1994 г.). Доказано, что исчисление Ламбека, обогащённое операцией аддитивной дизъюнкции, неполно относительно любого класса моделей на дистрибутивных решётках; тот же результат получен в коммутативном случае. Доказано, что грамматики, основанные на исчислении Ламбека с одним делением и аддитивной дизъюнкцией, порождают все конечные пересечения контекстно-свободных языков. Доказано, что проблема выводимости в исчислении Ламбека с одним делением, обогащённом субструктурной модальностью, допускающей правило перестановки или правила перестановки и сокращения, NP-полна. Для фрагмента атомарной теории решёток Клини, где операция пересечения допускается только в правых частях неравенств, построено исчисление циклического типа и доказана алгоритмическая разрешимость. Доказана алгоритмическая неразрешимость исчисления категориальных грамматик, на котором основана система CatLog3 (Моррилл, 2018-19). В области математической лингвистики Разработан алгоритм распознавания и заполнения эллипсиса для русского языка на основе контекстных представлений слов и нейронных сетей. Разработан алгоритм морфологического анализа для эвенкийского и селькупского языков, демонстрирующий наилучшие результаты для данный выборок. Разработан алгоритм деления на морфемы, использующий посимвольные языковые модели и показавший наилучшие результаты на 8 выборках малого размера из различных языков. Разработана адаптация векторных представлений типа BERT для задач морфологического и синтаксического анализа, показавший наилучшие результаты из известных моделей для русского языка. В области теории множеств Получено эффективное описание в теории ZF (без аксиомы выбора) нестандартного расширения поля вещественных чисел, для которого существует неглавный ультрафильтр над натуральным рядом, имеющий вполне упорядоченную базу. Найдена определимая функция, которая для любого проективного уровня делает счётным первый конструктивный несчётный кардинал.
5 1 января 2020 г.-31 декабря 2020 г. Алгоритмические и семантические вопросы математической логики. 2020
Результаты этапа: Доказано, что для определения общей информации в бесконечных последовательностях, данного Л.Левиным в 1974 году, выполнен Закон сохранения информации относительно преобразований вероятностными алгоритмами. Получено новое доказательство неарифметичности логики предикатов, основанной на понятии примитивно рекурсивной реализуемости для языка базисной арифметики, введенном С.Салехи в 2000 году. Им доказана теорема о корректности базисного исчисления предикатов относительно примитивно рекурсивной реализуемости. Опираясь на эту теорему и перевод интуиционистской логики в базисную, предложенный М.Ардеширом, в 2001 году Д.А.Витер доказал неарифметичность предикатной логики примитивно рекурсивной реализуемости. Его доказательство является технически чрезмерно сложным. Получено идейно более простое и прозрачное доказательство теоремы Витера. Рассматривался пропозициональный фрагмент HC объединенной логики задач и высказываний, введенной C. A. Мелиховым. Строятся модели типа Крипке для этой логики, доказывается полнота логики HC относительно таких моделей, а также свойство конечных моделей. Рассмотрены примеры применения моделей типа Крипке логики HC для решения некоторых вопросов (в частности, доказательство того, что HC является консервативным расширением логики H4). Также показано, что логика HC полна относительно шкал Крипке с проверяющими мирами, введенных С. Н. Артёмовым и Т. Протопопеску.

Прикрепленные к НИР результаты

Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".