Abstract

We have developed an interactive proof system for Map Theory using the generic theorem prover Isabelle. Within the system, we have formalized the development of ZFC from first principles, as well as a non-trivial part of elementary number theory, allowing us to prove that the rationals are linearly ordered field. The dissertation describes the proof techniques used, and in particular describes the type system developed to facilitate typed rewriting in a fundamentally untyped logic. Finally, the actual implementation is sketched.

Files

BibTeX Entry

@phdthesis
{
	skalberg:isabelle-mt,
	author = "Sebastian C[hristian] Skalberg",
	title = "An Interactive Proof System for Map Theory",
	school = "University of Copenhagen",
	year = "2002",
	month = oct,
	url = "http://www.mangust.dk/skalberg/phd/",
	postscript = "http://www.mangust.dk/skalberg/phd/skalberg-phd.ps",
	pdf = "http://www.mangust.dk/skalberg/phd/skalberg-phd.pdf",
	dvi = "http://www.mangust.dk/skalberg/phd/skalberg-phd.dvi",
}