Tautology Checkers in Isabelle and Haskell.
Jørgen Villadsen · Technical University of Denmark, DTU Orbit (Technical University of Denmark, DTU) · 2020
With the purpose of teaching functional programming and automated reasoning to computer science students, we formally verify a sound, complete and terminating tautology checker in Isabelle with code generation to Haskell.We describe a series of approaches and finish with a formalization based on formulas in negation normal form where the Isabelle/HOL functions consist of just 4 lines and the Isabelle/HOL proofs also consist of just 4 lines.We investigate the generated Haskell code and present a 24-line manually assembled program.