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 |