A Formulation of Classical Higher-Order Logic in Isabelle/Pure

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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 languageEnglish
Title of host publicationProceedings of Logic & Artificial Intelligence
PublisherVladimir Andrunachievici Institute of Mathematics and Computer Science
Publication date2023
ISBN (Print)978-9975-68-484-2
Publication statusPublished - 2023
EventLogic and Artificial Intelligence 2022 - Virtual
Duration: 12 Jan 202216 Jan 2022


ConferenceLogic and Artificial Intelligence 2022


Dive into the research topics of 'A Formulation of Classical Higher-Order Logic in Isabelle/Pure'. Together they form a unique fingerprint.

Cite this