メタ情報

http://fm.mizar.org/contents.html より：

• Title: Tarski Grothendieck Set Theory
• Author: Andrzej Trybulec
• Year: 1990
• Identifier: TARSKI
• PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf

Summary:

This is the first part of the axiomatics of the Mizar system. It includes the axioms of the Tarski Grothendieck set theory. They are: the axiom stating that everything is a set, the extensionality axiom, the definitional axiom of the singleton, the definitional axiom of the pair, the definitional axiom of the union of a family of sets, the definitional axiom of the boolean (the power set) of a set, the regularity axiom, the definitional axiom of the ordered pair, the Tarski's axiom~A introduced in \cite{TARSKI:1} (see also \cite{TARSKI:2}), and the Fr\ae nkel scheme. Also, the definition of equinumerosity is introduced.

bibtexエントリー http://fm.mizar.org/fm.bib より

@ARTICLE(TARSKI.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Tarski {G}rothendieck Set Theory},
      JOURNAL = {Formalized Mathematics},
      URL     = {http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf},
      YEAR    = {1990},
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {9--11})

https://arxiv.org/pdf/1505.01577.pdf より

• Title: Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
• Authors: Kazuhisa Nakasho, Yasunari Shidama
• Keywords: Mizar, mathematical knowledge management, search system, documentation generator

@ARTICLE(DocGenHtmlMizarLib,
      AUTHOR  = {Nakasho, Kazuhisa and Shidama Yasunari},
      TITLE   = {Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library},
      KEYWORDS= {Mizar, mathematical knowledge management, search system, documentation generator},
      URL     = {https://arxiv.org/pdf/1505.01577.pdf},
      YEAR    = {2015})