検索結果 1 件
デジタル規格・テクニカルリポート類
インターネットで読める全国の図書館
- 要約等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 f......gures 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.
- 一般注記出版タイプ： AM
- 関連情報RIFIS Technical Report || 91 || p1-4 http://www.i.kyushu-u.ac.jp/research/report.html