在 SMODELS 系统中自动验证弱等价性

在答案集编程（ASP）中，问题在于（i）编写逻辑程序，其答案集对应于问题的解，以及（ii）使用答案集求解器作为搜索引擎来计算程序的答案集。通常，程序员会创建一系列逐步改进的逻辑程序以优化特定求解器上的程序长度和执行时间。这导致程序员面临一个元问题：确保这些程序等价，即它们产生相同的答案集。为降低答案集编程的方法论层次的难度，我们提出一种基于翻译的方法，用于验证逻辑程序的等价性。基本思想是将待比较的逻辑程序P和Q翻译到单个逻辑程序EQT(P,Q)，其答案集（若存在）将给出P和Q等价性的反例。本文在更一般的设置下开发了该方法，充分考虑了在比较答案集时对原子可见性的处理。本文所述的翻译方法已实现为名为lpeq的翻译器，可在smode系统中使用相同的搜索引擎验证逻辑程序的弱等价性。我们的实验结果表明，该方法在某些情况下比直接交叉检查答案集更快地建立逻辑程序的等价性。