Abstract
We describe a formulation of classical higher-order logic in Isabelle/Pure. It has successfully been used three times in a computer science course on automated reasoning and it allows students to study proofs of the Grandfather formula and Cantor’s theorem as well as dozens of standard illustrative examples.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of Logic & Artificial Intelligence |
| Publisher | Vladimir Andrunachievici Institute of Mathematics and Computer Science |
| Publication date | 2023 |
| Pages | 223-238 |
| ISBN (Print) | 978-9975-68-484-2 |
| Publication status | Published - 2023 |
| Event | Logic and Artificial Intelligence 2022 - Virtual Duration: 12 Jan 2022 → 16 Jan 2022 |
Conference
| Conference | Logic and Artificial Intelligence 2022 |
|---|---|
| City | Virtual |
| Period | 12/01/2022 → 16/01/2022 |