Tautology Checkers in Isabelle and Haskell

Jørgen Villadsen

Tautology Checkers in Isabelle and Haskell

Jørgen Villadsen

Department of Applied Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

376 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 language	English
Title of host publication	Proceedings of the 35^th Italian Conference on Computational Logic
Editors	Francesco Calimeri , Simona Perri , Ester Zumpano
Publisher	CEUR-WS
Publication date	2020
Pages	327-341
Publication status	Published - 2020
Event	35^th Edition of the Italian Conference on Computational Logic - Virtual event, Rende , Italy Duration: 13 Oct 2020 → 15 Oct 2020 Conference number: 35 https://cilc2020.demacs.unical.it/

Conference

Conference	35^th Edition of the Italian Conference on Computational Logic
Number	35
Location	Virtual event
Country/Territory	Italy
City	Rende
Period	13/10/2020 → 15/10/2020
Internet address	https://cilc2020.demacs.unical.it/

Series	CEUR Workshop Proceedings
Volume	2710
ISSN	1613-0073

Access to Document

FulltextFinal published version, 665 KB

OpenUrl availability

Full text

Cite this

@inproceedings{3f3054a1a6ef4e2ea24f2def79488a77,

title = "Tautology Checkers in Isabelle and Haskell",

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.",

author = "J{\o}rgen Villadsen",

year = "2020",

language = "English",

series = "CEUR Workshop Proceedings",

publisher = "CEUR-WS",

pages = "327--341",

editor = "{Calimeri }, Francesco and {Perri }, Simona and Ester Zumpano",

booktitle = "Proceedings of the 35th Italian Conference on Computational Logic",

note = "35<sup>th</sup> Edition of the Italian Conference on Computational Logic, CILC 2020 ; Conference date: 13-10-2020 Through 15-10-2020",

url = "https://cilc2020.demacs.unical.it/",

}

Tautology Checkers in Isabelle and Haskell. / Villadsen, Jørgen.
Proceedings of the 35^th Italian Conference on Computational Logic. ed. / Francesco Calimeri ; Simona Perri ; Ester Zumpano. CEUR-WS, 2020. p. 327-341 (CEUR Workshop Proceedings, Vol. 2710).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Tautology Checkers in Isabelle and Haskell

AU - Villadsen, Jørgen

N1 - Conference code: 35

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

M3 - Article in proceedings

T3 - CEUR Workshop Proceedings

SP - 327

EP - 341

BT - Proceedings of the 35th Italian Conference on Computational Logic

A2 - Calimeri , Francesco

A2 - Perri , Simona

A2 - Zumpano, Ester

PB - CEUR-WS

T2 - 35<sup>th</sup> Edition of the Italian Conference on Computational Logic

Y2 - 13 October 2020 through 15 October 2020

ER -

Tautology Checkers in Isabelle and Haskell

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this