Animated logic: Correct functional conversion to conjunctive normal form

Research output: Contribution to journalConference articlepeer-review

1 Citation (Scopus)

Abstract

Computational Logic is "the calculus of Computer Science" and is an essential field of this area. Courses on this subject are usually either too informal (only providing pseudo-code specifications) or overly formal (merely presenting rigorous mathematical definitions) when describing algorithms. In either case, there is an emphasis on paper-and-pencil definitions and proofs rather than on computational approaches. It is seldom the case where these courses present executable code, even if the pedagogical advantages of using tools are well known. In this paper, we present an approach to obtain formally verified implementations of classical Computational Logic algorithms. The chosen tool for this approach is the Why3 platform since it allows implementing functions very close to their mathematical definitions, as well as it concedes a high degree of automation in the verification process. As proof of concept, we implement and prove the conversion algorithms from propositional formulae to conjunctive normal form. We apply our proposal on two variants of the algorithm: one in direct-style and another with an explicit stack structure. Being both first-order, Why3 processes the proofs straightforwardly.

Original languageEnglish
Pages (from-to)1-20
Number of pages20
JournalCEUR Workshop Proceedings
Volume2752
Publication statusPublished - 2020
EventJoint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 - Virtual, Paris, France
Duration: 5 Jul 2020 → …

Keywords

  • Computational Logic
  • Conjunctive Normal Form
  • Conversion Algorithm
  • Deductive Program Verification
  • Functional Programming
  • Why3

Fingerprint

Dive into the research topics of 'Animated logic: Correct functional conversion to conjunctive normal form'. Together they form a unique fingerprint.

Cite this