Using Isabelle in Two Courses on Logic and Automated Reasoning

Jørgen Villadsen*, Frederik Krogsdal Jacobsen

*Corresponding author for this work

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

192 Downloads (Pure)


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 languageEnglish
Title of host publicationFormal Methods Teaching
Publication date2021
ISBN (Print)978-3-030-91549-0
Publication statusPublished - 2021
Event4th International Workshop and Tutorial: 24th International Symposium on Formal Methods - Virtual Event
Duration: 21 Nov 202121 Nov 2021
Conference number: 4


Workshop4th International Workshop and Tutorial
LocationVirtual Event
OtherThe 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.
SeriesLecture Notes in Computer Science


  • Logic
  • Automated reasoning
  • Proof assistant Isabelle


Dive into the research topics of 'Using Isabelle in Two Courses on Logic and Automated Reasoning'. Together they form a unique fingerprint.

Cite this