EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (125 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA721953
Titel Any two countable, densely ordered sets without endpoints are isomorphic - a formal proof with KIV.
Autor Giese, Martin
Schoenegge, Arno
Institution Fakultät für Informatik (INFORMATIK)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1995
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,50.)
Abstract
Georg Cantor in 1895 gave the first (informal) proof for the fact that
any two countable, densely ordered sets without endpoints are isomorphic.
Here we report on a fully formal proof of this fact constructed
interactively with the KIV system (Karlsruhe Interactive Verifier).