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

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

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

Conference

ConferenceLogic and Artificial Intelligence 2022
CityVirtual
Period12/01/202216/01/2022

Fingerprint

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

Cite this