Solving two problems in general topology via types. (English) Zbl 1172.03309

Filliâtre, Jean-Christophe (ed.) et al., Types for proofs and programs. International workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-31428-8/pbk). Lecture Notes in Computer Science 3839, 138-153 (2006).
Summary: In the paper we show, based on two problems in general topology (Kuratowski closure-complement and Isomichi’s classification of condensed subsets), how typed objects can be used instead of untyped text to better represent mathematical content understandable both for human and computer checker. We present mechanism of attributes and clusters reimplemented in Mizar fairly recently to fit authors’ expectations. The problem of knowledge reusability which is crucial if we develop a large unified repository of mathematical facts, is also addressed.
For the entire collection see [Zbl 1099.68003].


03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)


Full Text: DOI