m-hiyama-memo https://blog.hatena.ne.jp/m-hiyama-memo/ (保存用) 檜山正幸のキマイラ飼育記 メモ編 https://m-hiyama-memo.hatenablog.jp/ Mizar 気付いた 用語法 記述書式（format） 述語や関数を呼び出すときの記述形式、定義時に指定する。 座（ローカス、ローサイ）（locus, loci） 述語や関数のパラメータ宣言 パターン 記述書式と関係あるようだが現在は不明 Mizarでは公理と定理の区別がなく、すべて定理： 公理定理： 証明なしで認める定理 定義定理： 述語定義から自動的に生成される定理。by definitionの根拠（justificatio）となる定理。 証明付き定理： proofブロックで正当化（justify）された定理 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fm-hiyama-memo.hatenablog.jp%2Fentry%2F20161214%2F1481683496" title="説明不足だが大事な用語 - (保存用) 檜山正幸のキマイラ飼育記 メモ編" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2016-12-14 11:44:56 rich https://m-hiyama-memo.hatenablog.jp/entry/20161214/1481683496 1.0 100%