Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

Jørgen Villadsen; Asta Halkjær From; Patrick Blackburn

doi:10.4204/EPTCS.354.6

Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

Jørgen Villadsen, Asta Halkjær From, Patrick Blackburn

Roskilde University

Research output: Contribution to journal › Journal article › Research › peer-review

95 Downloads (Pure)

Abstract

We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.

Original language	English
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	354
Pages (from-to)	71-85
ISSN	2075-2180
DOIs	https://doi.org/10.4204/EPTCS.354.6
Publication status	Published - 2022
Event	10^th International Workshop on Theorem proving components for Educational software - Carnegie Mellon University, Pittsburgh, United States Duration: 11 Jul 2021 → 11 Jul 2021

Conference

Conference	10^th International Workshop on Theorem proving components for Educational software
Location	Carnegie Mellon University
Country/Territory	United States
City	Pittsburgh
Period	11/07/2021 → 11/07/2021

Access to Document

10.4204/EPTCS.354.6

FulltextFinal published version, 928 KB

OpenUrl availability

Full text

Cite this

@article{0c0994210f8d489096174dfb937df6fb,

title = "Teaching Intuitionistic and Classical Propositional Logic Using Isabelle",

abstract = "We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.",

author = "J{\o}rgen Villadsen and From, {Asta Halkj{\ae}r} and Patrick Blackburn",

year = "2022",

doi = "10.4204/EPTCS.354.6",

language = "English",

volume = "354",

pages = "71--85",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

note = "10<sup>th</sup> International Workshop on Theorem proving components for Educational software, ThEdu'21 ; Conference date: 11-07-2021 Through 11-07-2021",

}

TY - JOUR

T1 - Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

AU - Villadsen, Jørgen

AU - From, Asta Halkjær

AU - Blackburn, Patrick

PY - 2022

Y1 - 2022

N2 - We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.

AB - We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.

U2 - 10.4204/EPTCS.354.6

DO - 10.4204/EPTCS.354.6

M3 - Journal article

SN - 2075-2180

VL - 354

SP - 71

EP - 85

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 10<sup>th</sup> International Workshop on Theorem proving components for Educational software

Y2 - 11 July 2021 through 11 July 2021

ER -

Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this