## ＜テクニカルレポート＞Degree-Two Formulas and Their Proofs

作成者 著者識別子 作成者名 所属機関 所属機関名 Department of Computer Science, College of General Education, Kyushu University 九州大学教養部 英語 Research Institute of Fundamental Information Science, Kyushu University 九州大学理学部附属基礎情報学研究施設 1991-11-07 49 Accepted Manuscript open access RIFIS Technical Report || 49 || p1-11 http://www.i.kyushu-u.ac.jp/research/report.html 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.続きを見る

### 本文ファイル

rifis-tr-49 pdf 602 KB 73

### 詳細

レコードID 3157 査読無 テクニカルレポート 2009.04.22 2017.01.20