Все выпуски

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

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.