Running a Prover in a Prover - Isabelle as a Meta-Logic

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

63 Downloads (Pure)


Isabelle provides a foundation of mathematics and I show how you can run your own verified prover directly in the Isabelle prover or as a stand-alone program. I describe the formalization of syntax and semantics and discuss the proof of soundness and completeness for a simple prover for first-order logic.
Original languageEnglish
Publication date2016
Number of pages1
Publication statusPublished - 2016
EventCADILLAC Workshop - Byens Lys Movie Theater, Fabriksområdet, Copenhagen, Denmark
Duration: 23 May 201125 May 2015


WorkshopCADILLAC Workshop
LocationByens Lys Movie Theater, Fabriksområdet
Internet address

Fingerprint Dive into the research topics of 'Running a Prover in a Prover - Isabelle as a Meta-Logic'. Together they form a unique fingerprint.

Cite this