Animated Logic: Correct Functional Conversion to Conjunctive Normal Form

Autor:	Barroso, Pedro, Pereira, Mário, Ravara, António
Rok vydání:	2020
Předmět:	Computer Science - Logic in Computer Science F.3.1
Druh dokumentu:	Working Paper
Popis:	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. Comment: 24 pages
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2003.05081 Zobrazit plný text záznamu View this record from Arxiv