Conference paper · Book chapter
Using Isabelle in Two Courses on Logic and Automated Reasoning
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2021 |
Pages: | 117-132 |
Proceedings: | 4<sup>th</sup> International Workshop and Tutorial |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | 4th International Workshop and Tutorial, Fmtea 2021, Virtual Event, November 21, 2021, Proceedings |
ISBN: | 3030915492 , 3030915506 , 9783030915490 and 9783030915506 |
ISSN: | 16113349 and 03029743 |
Types: | Conference paper and Book chapter |
DOI: | 10.1007/978-3-030-91550-6_9 |
ORCIDs: | Villadsen, Jørgen and Jacobsen, Frederik Krogsdal |