12/02/05 00:23:04.68
>>490
スレチじゃないと思いますね。
Coqはバージョンによって多少違うようですが、
シンタックスはCIC（帰納的構成計算）という型言語で出来ています。
Coqは帰納的な定理から型理論の導出規則に基づいて、
自動的に新たな定理を作る機能があります、等号公理以外についても。
URLﾘﾝｸ(www3.di.uminho.pt)
の23ページ位からですね。
12/02/05 00:23:04.68
>>490
スレチじゃないと思いますね。
Coqはバージョンによって多少違うようですが、
シンタックスはCIC（帰納的構成計算）という型言語で出来ています。
Coqは帰納的な定理から型理論の導出規則に基づいて、
自動的に新たな定理を作る機能があります、等号公理以外についても。
URLﾘﾝｸ(www3.di.uminho.pt)
の23ページ位からですね。