Все выпуски

В данной работе представлен новый подход к интерпретации логических формул для синтеза алгоритмов и программ. Предложенный метод сочетает в себе черты реализации Клини и интерпретации Гёделя «диалектика», но не опирается на них непосредственно. Рассматривается простой вариант позитивного языка логики предикатов без функций, с конъюнкцией, дизъюнкцией, импликацией и кванторами всеобщности и существования. Описана новая реализационная семантика формул и секвенций, в которой рассматривается не просто реализация формулы, а реализация с дополнительной поддержкой. Реализация примерно соответствует реализации Клини. Поддержка предоставляет дополнительные данные в пользу того, что реализация корректна. Поддержка должна подтвердить, что реализация работает корректно для формулы в любых корректных условиях применения. Представлен язык доказательств, для которого доказана теорема о корректности, показывающая, что любая выводимая секвенция имеет реализацию и поддержку, подтверждающую, что эта реализация работает правильно для этой формулы в любых корректных условиях при подходящем интерпретаторе используемых программ.

This paper presents a novel approach to interpreting logical formulas for synthesizing algorithms and programs. The proposed method combines features of Kleene realizability and Gödel's “dialectica” interpretation but does not rely on them directly. A simple version of positive predicate logic without functions is considered, including conjunction, disjunction, implication, and universal and existential quantifiers. A new realizability semantics for formulas and sequents is described, which considers not just a realization of a formula, but a realization with additional support. The realization roughly corresponds to Kleene realizability. The support provides additional data in favor of the correctness of the realization. The support must confirm that the realization works correctly for the formula under any valid conditions of application. A proof language is presented for which a correctness theorem is proved showing that any derivable sequent has a realization and support confirming that this realization works correctly for this formula under any valid conditions with a suitable interpreter for the programs used.

Рассматривается новое конструктивное понимание логических формул, согласованное с интуицией и с традиционными средствами конструктивного логического вывода. Новое понимание логически проще традиционной реализуемости (в смысле кванторной глубины), но является также естественным с точки зрения алгоритмического решения задач. Это понимание, кроме свидетельства (реализации, подтверждения) понимаемой формулы, привлекает понятия теста (противодействия, препятствия) этой реализации на данной формуле. Для понимания формулы $A$ рассматриваются предложения вида $a:A:b.$ Это предложение означает, что объект $a$ (выдвигаемый в подтверждение формулы $A$) выигрывает у объекта $b$ (который противодействует выполнению формулы $A$) формулу $A$ в процессе осуществления специальной процедуры сопоставления этих объектов друг с другом и с данной формулой. Данная процедура может считаться некоторой процедурой арбитража для вынесения необходимого решения. Базис процедуры арбитража для атомарных формул задается интерпретацией языка. Процедура для сложных предложений задается специальными правилами определения смысла логических связок. При наиболее естественном определении процедура арбитража имеет полиномиальную временную сложность. Формула $A$ считается истинной в новом смысле этого слова, если имеется подтверждение, выигрывающее ее у всех возможных противодействий. Рассматривается логический язык без отрицаний. Доказана теорема о корректности в новом смысле традиционных интуиционистских аксиом и правил вывода. При этом рассматривается секвенциальное логическое исчисление, ориентированное на обратный метод поиска вывода.

A new constructive understanding of logical formulas is considered. This understanding corresponds to intuition and traditional means of constructive logical inference. The new understanding is logically simpler than traditional realizability (in the sense of quantifier depth), but it also natural with respect to algorithmic solution of tasks. This understanding uses not only witness (realization) of the formula to understand but it also uses notion of test (counteraction) of this realization at the given formula. The main form of a sentence to understand a formula $A$ is $a:A:b$, that means that “the witness $a$ wins the obstacle $b$ while trying to approve the formula $A$”. This procedure can be regarded as a procedure of arbitration for making the necessary solution. The basis of the arbitration procedure for atomic formulas is defined by the interpretation of the language. The procedure for complex sentences is given by special rules determining the meaning of logical connectives. In the most natural definition of the arbitration procedure it has polynomial time complexity. A formula $A$ is considered to be true in the new sense if there is a witness of the formula that wins all possible obstacles at the formula. A language without negation is considered. A theorem of correctness of traditional intuitionistic axioms and inference rules is proved. The system of logical inference is formulated in sequent form. It is oriented to the inverse method of logical inference search.

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

The study of emotional text analysis today is one of the most interesting and developing areas. The emotions presented in the text and their analysis are a special topic of our interest. In this article, we will explore the various modal judgments in logic, the emotional model and their connection with the analysis of emotions. We will offer interpretations of some simple modalities in connection with information technologies for analyzing emotions in texts. We will expand the logic of the possible worlds; our modalities will better explain and comprehend this logic of the perceived state of the environment. We are presenting the logical formulas for defining the most common modalities for analyzing emotions from text. Our work is a continuation of the work done on modalities with more flexibility and completeness. The paper discusses the logical properties of emotional modalities, the logic of emotional evaluations and the definition of various modalities for analyzing emotions. We propose six different definitions of modalities and use three theorems to prove our hypothesis. This methodology also sets the directions for future research on logical modalities for analyzing emotions from text.