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

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

63 Downloads (Pure)

Abstract

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
http://cadillac.compute.dtu.dk/

Workshop

WorkshopCADILLAC Workshop
LocationByens Lys Movie Theater, Fabriksområdet
CountryDenmark
CityCopenhagen
Period23/05/201125/05/2015
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