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 | |
| Publication status | Published - 2021 |
| Event | 4th International Workshop and Tutorial: 24th International Symposium on Formal Methods - Virtual Event Duration: 21 Nov 2021 → 21 Nov 2021 Conference number: 4 |
Workshop
| Workshop | 4th 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