Using Isabelle in Two Courses on Logic and Automated Reasoning

Jørgen Villadsen; Frederik Krogsdal Jacobsen

doi:10.1007/978-3-030-91550-6_9

Using Isabelle in Two Courses on Logic and Automated Reasoning

Jørgen Villadsen^*
, Frederik Krogsdal Jacobsen

^*Corresponding author for this work

Department of Applied Mathematics and Computer Science

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

583 Downloads (Orbit)

Abstract

We present our experiences teaching two courses on formal methods and detail the contents of the courses and their positioning in the curriculum. The first course is a bachelor course on logical systems and logic programming, with a focus on classical first-order logic and automatic theorem proving. The second course is a master course on automated reasoning, with a focus on classical higher-order logic and interactive theorem proving. The proof assistant Isabelle is used in both courses, using Isabelle/Pure as well as Isabelle/HOL. We describe our online tools to be used with Isabelle/HOL, in particular the Sequent Calculus Verifier (SeCaV) and the Natural Deduction Assistant (NaDeA). We also describe our innovative Students’ Proof Assistant which is formally verified in Isabelle/HOL and integrated in Isabelle/jEdit using Isabelle/ML.

Original language	English
Title of host publication	Formal Methods Teaching
Publisher	Springer
Publication date	2021
Pages	117-132
ISBN (Print)	978-3-030-91549-0
DOIs	https://doi.org/10.1007/978-3-030-91550-6_9
Publication status	Published - 2021
Event	4^th International Workshop and Tutorial: 24th International Symposium on Formal Methods - Virtual Event Duration: 21 Nov 2021 → 21 Nov 2021 Conference number: 4

Workshop

Workshop	4^th International Workshop and Tutorial
Number	4
Location	Virtual Event
Period	21/11/2021 → 21/11/2021
Other	The FMTea21 workshop, affiliated with FM 2021, the 24th International Symposium on Formal Methods, Beijing, was held only online in November 2021, with proceedings published as Springer LNCS 13122.

Series	Lecture Notes in Computer Science
Volume	13122
ISSN	0302-9743

Keywords

Logic
Automated reasoning
Proof assistant Isabelle

Access to Document

10.1007/978-3-030-91550-6_9

FulltextAccepted author manuscript, 217 KB

OpenUrl availability

Full text

Cite this

@inproceedings{fecc4c61cc634a03aa1c4d0738f2a200,

title = "Using Isabelle in Two Courses on Logic and Automated Reasoning",

abstract = "We present our experiences teaching two courses on formal methods and detail the contents of the courses and their positioning in the curriculum. The first course is a bachelor course on logical systems and logic programming, with a focus on classical first-order logic and automatic theorem proving. The second course is a master course on automated reasoning, with a focus on classical higher-order logic and interactive theorem proving. The proof assistant Isabelle is used in both courses, using Isabelle/Pure as well as Isabelle/HOL. We describe our online tools to be used with Isabelle/HOL, in particular the Sequent Calculus Verifier (SeCaV) and the Natural Deduction Assistant (NaDeA). We also describe our innovative Students{\textquoteright} Proof Assistant which is formally verified in Isabelle/HOL and integrated in Isabelle/jEdit using Isabelle/ML.",

keywords = "Logic, Automated reasoning, Proof assistant Isabelle",

author = "J{\o}rgen Villadsen and Jacobsen, \{Frederik Krogsdal\}",

year = "2021",

doi = "10.1007/978-3-030-91550-6\_9",

language = "English",

isbn = "978-3-030-91549-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "117--132",

booktitle = "Formal Methods Teaching",

note = "4<sup>th</sup> International Workshop and Tutorial : 24th International Symposium on Formal Methods, FMTea 2021 ; Conference date: 21-11-2021 Through 21-11-2021",

}

TY - GEN

T1 - Using Isabelle in Two Courses on Logic and Automated Reasoning

AU - Villadsen, Jørgen

AU - Jacobsen, Frederik Krogsdal

N1 - Conference code: 4

PY - 2021

Y1 - 2021

N2 - We present our experiences teaching two courses on formal methods and detail the contents of the courses and their positioning in the curriculum. The first course is a bachelor course on logical systems and logic programming, with a focus on classical first-order logic and automatic theorem proving. The second course is a master course on automated reasoning, with a focus on classical higher-order logic and interactive theorem proving. The proof assistant Isabelle is used in both courses, using Isabelle/Pure as well as Isabelle/HOL. We describe our online tools to be used with Isabelle/HOL, in particular the Sequent Calculus Verifier (SeCaV) and the Natural Deduction Assistant (NaDeA). We also describe our innovative Students’ Proof Assistant which is formally verified in Isabelle/HOL and integrated in Isabelle/jEdit using Isabelle/ML.

AB - We present our experiences teaching two courses on formal methods and detail the contents of the courses and their positioning in the curriculum. The first course is a bachelor course on logical systems and logic programming, with a focus on classical first-order logic and automatic theorem proving. The second course is a master course on automated reasoning, with a focus on classical higher-order logic and interactive theorem proving. The proof assistant Isabelle is used in both courses, using Isabelle/Pure as well as Isabelle/HOL. We describe our online tools to be used with Isabelle/HOL, in particular the Sequent Calculus Verifier (SeCaV) and the Natural Deduction Assistant (NaDeA). We also describe our innovative Students’ Proof Assistant which is formally verified in Isabelle/HOL and integrated in Isabelle/jEdit using Isabelle/ML.

KW - Logic

KW - Automated reasoning

KW - Proof assistant Isabelle

U2 - 10.1007/978-3-030-91550-6_9

DO - 10.1007/978-3-030-91550-6_9

M3 - Article in proceedings

SN - 978-3-030-91549-0

T3 - Lecture Notes in Computer Science

SP - 117

EP - 132

BT - Formal Methods Teaching

PB - Springer

T2 - 4<sup>th</sup> International Workshop and Tutorial

Y2 - 21 November 2021 through 21 November 2021

ER -

Using Isabelle in Two Courses on Logic and Automated Reasoning

Abstract

Workshop

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this