檜山正幸のキマイラ飼育記 メモ編 このページをアンテナに追加 RSSフィード

この「はてなダイアリー」は、
2019年1月18日の記事を最後に更新を停止します。
しかし、
「檜山正幸のキマイラ飼育記 メモ編」は保存され、新規ブログに移行します。
新しい「檜山正幸のキマイラ飼育記」と関連ブログについては、
こちらの記事 をごらんください。
連絡は hiyama{at}chimaira{dot}org へ。

2016-12-13(火)

メタ情報

| 15:44 |

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

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})