动画逻辑：函数到合取范式的正确转换
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
摘要：
我们提出了一种方法来获得正式验证的经典计算逻辑算法的实现。我们选择Why3平台是因为它允许以非常接近数学定义的方式实现函数，并且它允许在验证过程中实现高度自动化。作为概念的证明，我们提出了一个数学定义的算法转换命题公式合取范式，实现WhyML（Why3语言，非常类似于OCaml），并证明实现的正确性。我们将我们的建议应用于该算法的两个变体：一个是直接风格，另一个是显式堆栈结构。作为两个一阶版本，Why3自然地处理证明。
英文摘要：
We present an approach to obtain formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform because it allows to implement functions in a style very close to the mathematical definitions, as well as it allows a high degree of automation in the verification process. As proof of concept, we present a mathematical definition of the algorithm to convert propositional formulae to conjunctive normal form, implementations in WhyML (the Why3 language, very similar to OCaml), and proofs of correctness of the implementations. We apply our proposal on two variants of this algorithm: one in direct-style and another with an explicit stack structure. Being both first-order versions, Why3 processes the proofs naturally.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
