一种面向目标导向答案集编程的抽象解释方法
An Approach to the Abstract Interpretation of Goal-Directed Answer Set Programming
浏览论文内容
中文总结 AI 辅助
该研究针对目标导向答案集编程，提出基于PLAI不动点的自顶向下算法及共享约束抽象域，通过三个应用研究其在s(CASP)中的实用性，证明编译时静态分析可改进目标导向ASP程序评估。
中文摘要 AI 辅助
抽象解释通过对程序语义的过度近似来推断和验证程序属性。它在（约束）逻辑编程中非常成功，能分析确定性、类型、别名和资源使用等，还用于验证和程序优化。但尚未在目标导向答案集编程（ASP）中研究。本文朝此迈出第一步，提出基于PLAI不动点的自顶向下算法，在Ciao Prolog预处理器的抽象解释器中实现，对目标导向ASP进行抽象解释。引入共享约束抽象域捕捉约束引发的变量潜在关系。通过三个应用研究该方法在s(CASP)中的实用性，结果表明编译时静态分析可改进目标导向ASP程序的评估。
英文摘要
Abstract Interpretation infers and verifies program properties by over-approximating program semantics. It has been highly successful for (Constraint) Logic Programming, enabling the analysis of determinism, types, aliasing, and resource usage, as well as application in verification and program optimization. However, Abstract Interpretation has not yet been studied in the context of Goal Directed Answer Set Programming (ASP). In this work, we take a first step in this direction. We present a top-down algorithm based on the PLAI fixpoint, implemented in the abstract interpreter of the Ciao Prolog Preprocessor, to perform abstract interpretation of goal-directed ASP. We also introduce the Shared-Constraints abstract domain, designed to capture potential relations among variables induced by constraints. Finally, we study the practicality of the approach in s(CASP) through three applications: detection of false odd loops over negation, efficient forall evaluation enabled by the Shared-Constraints domain, and abstract specialization (including the simplification of required global constraints). Our results show that compile-time static analysis can improve the evaluation of goal-directed ASP programs.
