With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it would be desirable to have a tool which can automatically verify whether an optimised subprogram can replace the original subprogram. Formally this corresponds to the problem of verifying the strong equivalence of two programs. In order to do so, the translation tool anthem was developed. It can be used in conjunction with an automated theorem prover for classical logic to verify that two programs are strongly equivalent. With the current version of anthem, only the strong equivalence of positive programs with a restricted input language can be verified. This is a result of the translation $\tau^*$ implemented in anthem that produces formulas in the logic of here-and-there, which coincides with classical logic only for positive programs. This thesis extends anthem in order to overcome these limitations. First, the transformation $\sigma^*$ is presented, which transforms formulas from the logic of here-and-there to classical logic. A theorem formalises how $\sigma^*$ can be used to express equivalence in the logic of here-and-there in classical logic. Second, the translation $\tau^*$ is extended to programs containing pools. Another theorem shows how $\sigma^*$ can be combined with $\tau^*$ to express the strong equivalence of two programs in classical logic. With $\sigma^*$ and the extended $\tau^*$, it is possible to express the strong equivalence of logic programs containing negation, simple choices, and pools. Both the extended $\tau^*$ and $\sigma^*$ are implemented in a new version of anthem. Several examples of logic programs containing pools, negation, and simple choice rules, which the new version of anthem can translate to classical logic, are presented. Some a...

翻译：随着回答集编程在工业应用中的增长，特别是在关键应用领域，对形式化验证工具的需求也随之增加。在程序优化过程中，理想的工具是能够自动验证优化后的子程序是否可以替换原始子程序。从形式上看，这对应于验证两个程序的强等价性问题。为此，开发了翻译工具anthem，该工具可与经典逻辑的自动定理证明器结合使用，以验证两个程序是否强等价。当前版本的anthem仅能验证具有受限输入语言的正程序的强等价性，这是因其实现的翻译$\tau^*$会产生“此处与彼处逻辑”公式，而该公式仅对正程序与经典逻辑一致。本论文旨在扩展anthem以克服这些限制。首先，提出变换$\sigma^*$，它将公式从“此处与彼处逻辑”转换为经典逻辑，并通过定理形式化说明了如何利用$\sigma^*$在经典逻辑中表达“此处与彼处逻辑”的等价性。其次，将翻译$\tau^*$扩展至包含池（pools）的程序，另一定理展示了如何将$\sigma^*$与$\tau^*$结合，在经典逻辑中表达两个程序的强等价性。通过$\sigma^*$和扩展后的$\tau^*$，可表达包含否定、简单选择（simple choices）和池的逻辑程序的强等价性。扩展后的$\tau^*$和$\sigma^*$均已在新版anthem中实现。本文展示了若干包含池、否定和简单选择规则的程序示例，新版anthem可将其翻译为经典逻辑。部分...