ИСТИНА

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

In the course of the work on the project, it is expected to study a number of issues related to non-classical semantics of logical and logical-mathematical languages, non-classical formal systems and their applications in mathematical linguistics and bioinformatics. The focus will be on the following issues: 1) the study of computational complexity of fragments of the Lambek calculus with modalities; 2) the study of justification logics defined by classes of precise basic models with different signature, the study of their axiomatization by means of the language of the logic of evidence; 3) the study of the constructive semantics of logical and logico-mathematical languages based on various versions of subrecursive and generalized computability; 4) the study of computational properties of superintuitionistic logics; 5) construction of a linear algorithm for the shortest transformation of loaded graphs with vertices of the 1st and 2nd degrees with fuzzy operations and the corresponding calculus, allowing one to establish the correctness of the algorithm.

Ожидается получение оценок класса языков, задаваемых грамматиками в исчислении Ламбека с факультативными делениями. Проект продолжает ряд исследований исчисления Ламбека с конъюнкцией и дизъюнкцией; результаты позволят оценить возможность использования факультативных делений для описания формальных языков, их распознающую силу. Ожидается построение исчислений, формализующих логики свидетельств, определяемые классами точных базисных моделей с различной сигнатурой, доказательство соответствующих теорем о полноте. В результате будет закрыт актуальный в настоящее время вопрос теории базисных моделей для логики свидетельств. Будет получено формальное обоснование «наивного» использования термов логики свидетельств для формализации эпистемических сценариев, посвященных анализу аргументации. Планируется доказать неарифметичность предикатной логики, основанной на понятии строго примитивно-рекурсивной реализуемости, обнаружить некорректность интуиционистской логики относительно минимальной реализуемости, доказать неарифметичность предикатной логики, основанной на понятии минимальной реализуемости. Эти результаты позволят восполнить имеющиеся пробелы в исследовании конструктивных семантик, основанных на субрекурсивной реализуемости. Предполагается разработка системы понятий для конструктивных семантик логических и логико-математических языков, основанных на понятии вычислимости, задаваемом достаточно произвольным классом функций V, выявление свойств класса V, при которых соответствующая ему предикатная конструктивная логика согласована с той или иной традиционной классической или неклассической (интуиционистской, базисной) логиками. Ожидаемые результаты должны внести значительный вклад в исследование неклассических логик. Ставится задача разработки метода интервалов для характеризации суперинтуиционистских пропозициональных логик. Ожидается получение описания синтаксических и семантических свойств суперинтуиционистских логик, для которых существуют неразрешимые расширения, а также логик, все расширения которых разрешимы. Планируется выявление свойств суперинтуиционистских логик, которые сами являются расширениями неразрешимых суперинтуиционистских логик. Ставится задача получения точной оценки минимального числа переменных в добавочной аксиоме неразрешимого суперинтуиционистского исчисления. Ожидается нахождение минимальной корректной сигнатуры формул, для которой существуют неразрешимые суперинтуиционистские логики. Планируется получение описания представительного класса суперинтуиционистских логик, сложность вывода в которых ограничена полиномом от сложности выводимой формулы. Ставится задача выявления возможности получения нижних оценок сложности вывода для суперинтуиционистских логик. Будет доказана линейность и корректность полной версии разработанного алгоритма кратчайшего преобразования нагруженных графов с вершинами 1-ой и 2-ой степеней с нечётко заданными операциями, что будет служить основанием для его эффективной реализации, ориентированной на распределенные вычисления. Востребованность такой работы подтверждается наличием большого числа эвристических подходов к той же задаче, в общем случае не обладающих указанными свойствами. Планируется доказать полноту по Крипке, финитную аппроксимируемость и разрешимость PDL-расширений широкого семейства полимодальных логик, построенных из одномодальных, обладающих тем или иным свойством допустимости фильтрации. Результаты могут найти применение при моделировании мультиагентных систем, в которых модальности, отвечающие разным агентам, подчиняются различным модальным логикам, которые, тем не менее, обладают свойством фильтруемости. Для дескрипционных логик, таких как ALC, ALCOIQ, SHIQ и других, используемых на практике для представления знаний в языке сетевых онтологий OWL (Web Ontology Language), предполагается исследовать понятие С-представимости конъюнктивных запросов и его зависимость от языков баз знаний, изучить его связь с понятием модальной определимости запроса и найти полный критерий С-представимости; изучить вопрос о том, всегда ли С-представимость (над счетными моделями) произвольной формулы первого порядка влечет ее модальную определимость.

В 2003 году М. Р. Пентус доказал , что по вычислительной сложности категориальные грамматики Ламбека соответствуют классу NP. В 2011 году М. Р. Пентус нашёл полиномиальный алгоритм для фрагмента монотонного исчисления Ламбека с одним делением. В.Н.Крупский (1997) аксиоматизировал функциональную логику доказательств FLP, вариант логики LP, основанный на арифметических интерпретациях с функциональным предикатом доказательств, и описал соответствующую ей символическую семантику, а также исследовал расширение логики FLP ссылочными конструкциями вида “та формула, которую доказывает x” (2006). В работах В.Е.Плиско (1977, 1990, 1999) разработаны методы применения теоремы Тенненбаума для исследования предикатных логик конструктивных математических теорий. А. Ю. Коноваловым установлена корректность базисной логики предикатов относительно арифметической и гиперарифметической реализуемостей и доказано, что семантика арифметической реализуемости для языка формальной арифметики совпадает со стандартной классической семантикой. Г. В. Боков получил окончательное решение ряда массовых проблем для пропозициональных исчислений. Им доказана алгоритмическая неразрешимость проблемы распознавания расширений для любого нетривиального пропозиционального исчисления. Полученный опыт моделирования алгоритмических проблем пропозициональными логиками позволил не только построить неразрешимое суперинтуиционистское пропозициональное исчисление с аксиомами от трех переменных, но и доказать экспоненциальную нижнюю оценку сложности вывода для ослабленного варианта систем Фреге. Имеются предварительные варианты алгоритма кратчайшего преобразования нагруженных графов с вершинами 1-ой и 2-ой степеней с нечётко заданными операциями и доказательства их линейности и корректности вместе с прикладными вычислениями на основе альфа-версии программы, выполненными Р.А. Гершгориным.