| 作成者 |
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
According to the formulas-as-types notion, an implicational formula can be identified with a type of a $ lambda $-term which represents a proof of the formula in implicational fragment of intuitionist...ic logic. A formula is balanced iff no type variable occurs more than twice in it. It is known that balanced formulas have unique proofs. In this paper, it is shown that closed $ lamda $-terms in $ \beta $-normal form having balanced types are BCK-$ lamda $-terms in which each variable occurs at most once. A formula is BCK-minimal iff it is BCK-provable and it is not a non-trivial substitution instance of other BCK-provable formula. It is also shown that the set BCK-minimal formulas is identical to the set of principal type-schemes of BCK-$ lamda $-terms in $ \beta $-$ eta $-normal form.続きを見る
|
Mendeley出力
rifis-tr-48