| 作成者 |
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
A reduction rule is introduced by $ x^ alpha \to \beta left(P^((alpha \to \beta)\to alpha) \to alpha y ^ (alpha \to \beta) \to alpha \right) stackrel{P}{\to} x(yx) $ as a transformation of proof figur...es in implicational classical logic. The proof figure are represented as typed $ lamda-terms $ with a new constant $ P^ left(( alpha \to \beta) \to alpha) \to alpha $. It is shown that all the terms with the same type are equivalent with respect to the $ \beta-reduction $ and this reduction. Hence all the proof of the same implicational formula are equivalent.続きを見る
|
Mendeley出力
rifis-tr-91