Abstract
In the last decade we have focused our main logic courses on proof assistants and related tools. We find that the modern computer science curriculum requires a focus on applications instead of just penand-paper proofs. Notably, we teach the metatheory of logic using tools with formalizations in proof assistants like Isabelle such that we have both implementations and theorems about them.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of LogTeach-22 |
| Number of pages | 3 |
| Publication date | 2022 |
| Publication status | Published - 2022 |
| Event | LogTeach-22 - Haifa, Israel Duration: 31 Jul 2022 → 1 Aug 2022 https://www.cs.technion.ac.il/~janos/LogTeach-22/ |
Conference
| Conference | LogTeach-22 |
|---|---|
| Country/Territory | Israel |
| City | Haifa |
| Period | 31/07/2022 → 01/08/2022 |
| Internet address |
Keywords
- Logic
- Automated Reasoning
- Isabelle Proof Assistant