Все выпуски

Эта статья представляет подход к дедуктивному синтезу программ с использованием секвенциального подхода Генцена в рамках логического программирования. Используя секвенциальное исчисление как формальную систему для структурированного логического вывода, наш метод автоматизирует вывод доказуемо корректных программ из спецификаций, выраженных в логике предикатов первого порядка без отрицаний. Мы формализуем синтаксис и семантику секвенциального исчисления, реализуя его основные правила вывода (правила введения и удаления) в виде предикатов в логическом программировании для обеспечения масштабируемого синтеза. Практические примеры демонстрируют преобразование логических спецификаций в исполняемые программы. Подход обеспечивает формальную корректность через конструктивную семантику реализуемости Клини, при этом синтезированные программы работают в субрекурсивном языке, чтобы гарантировать завершение вычислительных процессов. Мы оцениваем сильные стороны метода, включая его надежность для систем с критической безопасностью, и его ограничения, такие как вычислительная сложность для неограниченных конструкций. В сравнении с синтезом, управляемым ИИ, наш подход ставит на первое место формальные гарантии, дополняя современные тенденции. Направления будущих исследований включают оптимизацию вычислительной эффективности и расширение применимости к сложным задачам реального мира.

This article presents an approach to deductive program synthesis using Gentzen’s sequent calculus within the framework of logic programming. By leveraging sequent calculus as a formal system for structured logical inference, our method automates the derivation of provably correct programs from specifications expressed in negation-free first-order predicate logic. We formalize the syntax and semantics of sequent calculus, implementing its core inference rules (introduction and elimination rules) as predicates in logic programming to enable scalable synthesis. Practical examples demonstrate the transformation of logical specifications into executable programs. The approach ensures formal correctness through a constructive semantics inspired by Kleene's realizability, with synthesized programs operating in a subrecursive language to guarantee termination. We evaluate the method's strengths, including its reliability for safety-critical systems, and its limitations, such as computational complexity for unbounded constructions. Compared to AI-driven synthesis, our approach prioritizes formal guarantees, complementing modern trends like relational programming. Future research directions include optimizing computational efficiency and extending applicability to complex real-world problems.

В работе предлагается для формального описания и структурного анализа изображений использовать расширение $ \mathcal{ALC}(GI)$ дескрипционной логики $ \mathcal{ALC} $. Концепты и роли логики $ \mathcal{ALC} (GI)$ интерпретируются на графе изображения и его подграфах. Описана модель изображения в виде многослойного атрибутивного графа. Граф изображения содержит слой цветовых сегментов, слой границ, слой скелетонов. Каждый слой представляет собой планарный граф, слои связаны между собой отношениями «предок-потомок». Переход от пиксельного представления изображения к графовому позволяет существенно увеличить эффективность его анализа. Приведены примеры предметных терминологических аксиом, определяющих структурные элементы изображения и составленные из них буквы, а также результаты эксперимента, проведенного на задаче распознавания букв в слитном рукописном тексте.

In this paper, it's proposed to use the extension $\mathcal{ALC}(GI)$ of description logic $\mathcal{ALC}$ for the formal description and structural analysis of images. Concepts and the roles of $\mathcal{ALC}(GI)$ are interpreted on an image graph and its subgraphs. The model of image in the form of multi-layered attribute graph is presented. It contains a layer of color segments, a layer of boundaries and a layer of skeletons. Each layer is a planar graph, layers are linked by means of “ancestor-descendant” relations. The transition from the pixel representation of an image to the graph one allows us to increase the effectiveness of image analysis. Examples of terminological axioms that define structural elements of an image and letters composed of them, as well as the results of an experiment of recognizing letters in a cursive handwritten text are presented.

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

The article analyzes the disadvantages of Aristotle syllogistic basis. The author indicates reasons for paradoxes of tangible implication in classical logics. It is suggested to verify correlations between a conditioned judgment and a tangible implication. Such paradoxes are not allowed in the multi-level syllogistic orthogonal basis.