Tautology Checkers in Isabelle and Haskell

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

4 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 35th Italian Conference on Computational Logic
EditorsFrancesco Calimeri , Simona Perri , Ester Zumpano
PublisherCEUR-WS
Publication date2020
Pages327-341
Publication statusPublished - 2020
Event35th Edition of the Italian Conference on Computational Logic - Virtual event, Rende , Italy
Duration: 13 Oct 202015 Oct 2020
https://cilc2020.demacs.unical.it/

Conference

Conference35th Edition of the Italian Conference on Computational Logic
LocationVirtual event
CountryItaly
CityRende
Period13/10/202015/10/2020
Internet address
SeriesCEUR Workshop Proceedings
Volume2710
ISSN1613-0073

Fingerprint Dive into the research topics of 'Tautology Checkers in Isabelle and Haskell'. Together they form a unique fingerprint.

Cite this