高级逻辑程序中等价性质的自动验证——学士论文

随着使用答案集编程的工业应用的增加,对形式化验证工具的需求也随之增长,尤其是对于关键应用。在程序优化过程中,若有一个工具能自动验证优化后的子程序是否可以替换原始子程序,将十分理想。形式上,这对应于验证两个程序的强等价问题。为此,开发了翻译工具 anthem。它可与经典逻辑的自动定理证明器结合使用,以验证两个程序是否强等价。在 anthem 的当前版本中,只能验证具有受限输入语言的正程序的强等价。这是由于 anthem 中实现的翻译 $\tau^*$ 生成此处与彼处逻辑中的公式,而该逻辑仅对正程序与经典逻辑一致。本论文对 anthem 进行了扩展以克服这些限制。首先,提出了变换 $\sigma^*$,将此处与彼处逻辑中的公式转换为经典逻辑。一个定理形式化了如何使用 $\sigma^*$ 在经典逻辑中表达此处与彼处逻辑中的等价。其次,将翻译 $\tau^*$ 扩展到包含池的程序。另一个定理展示了如何将 $\sigma^*$ 与 $\tau^*$ 结合以在经典逻辑中表达两个程序的强等价。借助 $\sigma^*$ 和扩展的 $\tau^*$,可以表达包含否定、简单选择以及池的逻辑程序的强等价。扩展的 $\tau^*$ 和 $\sigma^*$ 均在新版 anthem 中实现。给出了若干包含池、否定和简单选择规则的逻辑程序示例,新版 anthem 可将其翻译为经典逻辑。一些 a...