Animated Logic: Correct Functional Conversion to Conjunctive Normal Form

TL;DR

This paper introduces a formally verified method for converting propositional formulas to conjunctive normal form using the Why3 platform, ensuring correctness through proofs for different algorithm variants.

Contribution

It provides a verified implementation of CNF conversion algorithms in WhyML, demonstrating correctness for both direct-style and stack-based approaches.

Findings

Verified correctness proofs for two CNF conversion algorithms

Implementation in WhyML closely follows mathematical definitions

Demonstrates automation capabilities of Why3 for formal verification

Abstract

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.