论文标题
动画逻辑：正确的功能转换为连接正常形式
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
论文作者
论文摘要
我们提出了一种获得经典计算逻辑算法正式验证的实现的方法。我们选择Why3平台，因为它允许以非常接近数学定义的样式实现功能，并且允许在验证过程中具有高度的自动化。 作为概念证明，我们提出了算法的数学定义，以将命题公式转换为结合性正常形式，在whyMl中的实现（Why3语言，与OCAML非常相似）以及实现的正确性证明。我们将建议应用于该算法的两个变体：一种直接风格，另一种具有明确的堆栈结构。对于这两个一阶版本，为什么3个自然处理证明。
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.
