Experiments with ZF Set Theory in HOL and Isabelle
Sten Agerholm
July 1995 |
Abstract:
Most general purpose proof assistants support versions of typed
higher order logic. Experience has shown that these logics are capable of
representing most of the mathematical models needed in Computer Science.
However, perhaps there exist applications where ZF-style set theory is more
natural, or even necessary. Examples may include Scott's classical
inverse-limit construction of a model of the untyped
![]() ![]() ![]() Available as PostScript, PDF, DVI. |