Speaker:
Jørgen Villadsen
 
Title:
Running a prover in a prover - Isabelle as a meta-logic
 
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.