.png){kind=icon}
.png){kind=icon}
Return
DEDUCTIVE PROGRAM SYNTHESIS USING LOGIC PROGRAMMING
.png){kind=icon}
PRE
AI
DOI：10.35634/vm260108.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
deductive synthesis
sequent calculus
logic programming
Prolog
logical inference
program-ming automation
artificial intelligence
Journal
V
IF:
0.7
Papers:
8
Citations:
0
