| アイテムタイプ |
レポート / Report(1) |
| 公開日 |
2019-03-12 |
| タイトル |
|
|
タイトル |
NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment |
|
言語 |
en |
| 言語 |
|
|
言語 |
eng |
| キーワード |
|
|
言語 |
ja |
|
主題Scheme |
Other |
|
主題 |
テクニカルレポート |
| キーワード |
|
|
言語 |
en |
|
主題Scheme |
Other |
|
主題 |
Technical Report |
| 資源タイプ |
|
|
資源 |
http://purl.org/coar/resource_type/c_6501 |
|
タイプ |
departmental bulletin paper |
| ID登録 |
|
|
ID登録 |
10.20736/0000001243 |
|
ID登録タイプ |
JaLC |
| 著者 |
龍田, 真
藤田, 憲悦
長谷川, 立
中野, 洋
|
| 抄録 |
|
|
内容記述タイプ |
Abstract |
|
内容記述 |
This paper shows the inhabitance in the lambda calculus with negation, product, and existential types is decidable. This is proved by showing existential quantification can be eliminated and reducing the problem to provability in intuitionistic propositional logic. By the same technique, this paper also shows existential quantification followed by negation can be replaced by a specific witness in both that system and the system with implication and bottom. |
|
言語 |
en |
| 書誌情報 |
ja : NIIテクニカル・レポート
en : NII Technical Report
p. 1-13,
発行日 2008-04-04
|
| 出版者 |
|
|
出版者 |
国立情報学研究所 |
|
言語 |
ja |
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1346-5597 |
NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment (249.4 kB)
