arXiv:2502.09230v1 声明类型: cross 摘要: 逻辑程序设计范式（ASP）是知识表示与推理领域的重要工具。作为一种简洁、人类可读且声明式的语言，ASP 是开发可信赖（特别是人工智能）软件系统的优秀工具。然而，正式验证 ASP 程序面临着一些独特的挑战，例如： 1. 缺乏模块性（规则的意义难以在脱离包含程序的情况下定义）， 2. 由输入数据决定的地面化和求解语义（规则的意义依赖于程序所涉及的数据）， 3. 现有工具的限制。 我的研究议程一直致力于解决这些问题，旨在使 ASP 验证成为一项可访问且常规的任务，该任务可以在程序开发过程中定期进行。在这个方向上，我已经研究了基于向此处-那里逻辑和多型一阶逻辑的 ASP 替代语义。这些语义促进了逻辑程序的模块化理解，回避了地面化步骤，并使我们能够使用自动定理证明器来自动验证程序的属性。