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

キマイラ・サイト
キマイラ飼育記 本編
メモ編のアーカイブ
檜山の公開プライベート(なんじゃそりゃ?)メモ
檜山本人以外の読者を考慮しておりません。あしからず。

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