<テクニカルレポート>
Degree-Two Formulas and Their Proofs

作成者
本文言語
出版者
発行日
収録物名
出版タイプ
アクセス権
関連DOI
関連URI
関連情報
概要 An implicational formula is said to be of degree two when it has tlze form $ alpha = left(a \frac{1}{1} \to...\to a \frac{1}{n_1} \to a^1 \right) \to ... \to left(a ^m_1 \to ... \to a^m_n_m \to a^m \r...ight) \to a $ with type variables $ a \frac{1}{1}, . . ., a \frac{1}{n_1},a~1,...,a^m_1,...,a^1_n_m,a^m and a left(n_1,...,n_m leq 0 \right) $ .Given a degree two formula $ alpha $, we construct, in polynormial time of the size of $ alpha $, a context free grammar $ G left(alpha \right) $ such that $ proof (alpha)= left{ N | N leftarrow lambda _x_1...x_m.M for some M in L (G(alpha)light} $ where proof $ (alpha)$ is the set of normal form proof of $ alpha $ in NJ (natural deduction system of intuitionistic logic) and $ L(G(alpha)) $ is the set of context free language generated by $ G(alpha) $. The set of provable formulas of degree two is characterized as the set of simple substitution instances of principal type-schemes of 'sorted' terms. $ A lambda -term lamda-term /lamda _x_1...x_m.M $ is sorted when M has no $ lamda $'s and is constructed from function symbols $ x_1, ... , x_m, $ of arity $ n_1,...n_m in $, in the sense of many sorted algebra.続きを見る

本文ファイル

pdf rifis-tr-49 pdf 602 KB 169  

詳細

レコードID
査読有無
タイプ
登録日 2009.04.22
更新日 2017.01.20

この資料を見た人はこんな資料も見ています