9.3 その用語が使用されている ABS ファイルを知る
9.3.1 grep を使う方法
その用語がライブラリのなかのどこで使われているか知りたいことがあります．それ は，(どこで定義されているのか)とか，(それに関する定理はどことどこにあるのか)と いった疑問のあるときです．そのようなときは，標準の MIZAR システムには入ってい ないのですが，egrep というプログラムを使うと便利です．例えば Metric
という用
語があらわれる ABS ファイルをリストアップするには，C:\>cd /mizar/abstr
C:\>/mizar/egrep Metric *.* \| more
とすればよいのです．egrep.exe
プログラムは，例えば，次の URL(インターネット
の)からフリーで入手できます(M.Patnode氏によるもの)．http://www.eunet.bg/simtel.net/msdos/txtutl.html
ディレクトリの移動を含めてバッチファイルにしておくと便利です．
また通常の文字列(英数字)を探すときは上記のようで良いのですが，一般にはその文 字列を正規表現 (regular expression) で探すことになっています．従って，a+b+c 又は
x+y+z のように 3
変数の和があるファイルと行を探すには，egrep [a-z]\ + [a-z]\ + [a-z] *.*
のようにしなくてはなりません．ここで
[a-z]
はアルファベット a から z までの文字のいずれかを表し，\+
は
+ の文字を表します．ここで，+
や
- のような記号は，バックスラッシュ \の後に書かなくてはいけない
ことに注意しましょう．正規表現の詳しい説明はインターネット上にたくさん出ています．例えば，
http://www.robelle.com/smugbook/regexpr.html
を参照してください．
9.3.2 Web から検索する方法
インターネットに接続できる環境にあれば，Web で検索することもできます．
ブラウザで
http://markun.cs.shinshu-u.ac.jp/Mirror/search_mml.html
という URL を開いてください．図
9.1
のような検索画面が表示されます．この画面で調べたい用語をタイプし（図
9.1
では Metric ），abstract fileから探すの か miz file から探すのか，あるいは両方から探すのかラジオボタンで選択して（図9.1
では
abstract file） search をクリックすることで検索できます．
図
9.1 Web
での検索画面Chapter 10
バージョンアップについて
MIZAR
のバージョンアップは頻繁に行われます．このとき，ライブラリの増加は当然のことで，自分の作成中の
article
のチェックに影響を及ぼしませんが，チェッカーの バージョンアップについては注意を要します．インターネットのMIZAR
のホームペー ジをよくウオッチングして，最新のものを入手するよう気を付けて下さい.時々，従来使っていた基本的な定理が cancel されてしまうことがあり，戸惑いますが，
新バージョンのディレクトリ中の
CANCELED.DOC
の中にその情報が書かれています．
Appendix A
予約語一覧表
and antonym attr
as assume be
begin being by canceled case cases cluster clusters coherence compatibility consider consistency constructors contradiction correctness
def deffunc definition definitions defpred end
environ equals ex existence for from
func given hence hereby requirements holds
if iff implies
is it let means mode not notation now of
or otherwise over
per pred proof
provided qua reconsider redefine reserve scheme schemes set st
struct such symmetry synonym take that
the then theorem theorems thesis thus
uniqueness vocabulary where