Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
CoRR(2024)
摘要
We show a projective Beth definability theorem for logic programs under the
stable model semantics: For given programs P and Q and vocabulary V (set
of predicates) the existence of a program R in V such that P ∪ R and
P ∪ Q are strongly equivalent can be expressed as a first-order
entailment. Moreover, our result is effective: A program R can be constructed
from a Craig interpolant for this entailment, using a known first-order
encoding for testing strong equivalence, which we apply in reverse to extract
programs from formulas. As a further perspective, this allows transforming
logic programs via transforming their first-order encodings. In a prototypical
implementation, the Craig interpolation is performed by first-order provers
based on clausal tableaux or resolution calculi. Our work shows how
definability and interpolation, which underlie modern logic-based approaches to
advanced tasks in knowledge representation, transfer to answer set programming.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要