Portal de Periódicos da CAPES

Using Isabelle in Two Courses on Logic and Automated Reasoning

2021; Springer Science+Business Media; Linguagem: Inglês

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

1611-3349

Jørgen Villadsen, Frederik Krogsdal Jacobsen,

Formal Methods in Verification

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.