用多类型逻辑重构ASP语义，实现可验证的模块化程序设计。
Relating Answer Set Programming and Many-sorted Logics for Formal Verification
- 将ASP翻译为这里-那里逻辑和多类型一阶逻辑，实现模块化理解
- 绕过依赖输入数据的求解过程，支持自动定理证明验证程序性质
- 适合需要形式化验证的可信人工智能系统开发者
答案集编程（ASP）是知识表示与推理领域的重要逻辑编程范式，以其简洁、易读的声明式语言特性，成为构建可信（尤其是人工智能）软件系统的优秀工具。然而，对ASP程序进行形式化验证面临三大挑战：1. 缺乏模块性（规则意义难以脱离整体程序独立定义）；2. 求解时接地语义（规则意义依赖于程序接地时的输入数据）；3. 现有工具局限。本研究旨在解决上述问题，使ASP验证成为可访问、常规化的开发环节。为此，探索基于向‘这里-那里’逻辑和多类型一阶逻辑转换的替代语义，促进逻辑程序的模块化理解，避免接地过程，并借助自动化定理证明器自动验证程序性质。
原文摘要 · Abstract (English)
Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。