{"created":"2021-03-01T05:52:57.451997+00:00","id":1243,"links":{},"metadata":{"_buckets":{"deposit":"8dc35028-28c5-4f11-b908-0688dc308e9d"},"_deposit":{"id":"1243","owners":[],"pid":{"revision_id":0,"type":"depid","value":"1243"},"status":"published"},"_oai":{"id":"oai:repository.nii.ac.jp:00001243","sets":["136"]},"author_link":[],"control_number":"1243","item_5_biblio_info_30":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2008-04-04","bibliographicIssueDateType":"Issued"},"bibliographicPageEnd":"13","bibliographicPageStart":"1","bibliographic_titles":[{"bibliographic_title":"NIIテクニカル・レポート","bibliographic_titleLang":"ja"},{"bibliographic_title":"NII Technical Report","bibliographic_titleLang":"en"}]}]},"item_5_description_28":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_5_identifier_registration":{"attribute_name":"ID登録","attribute_value_mlt":[{"subitem_identifier_reg_text":"10.20736/0000001243","subitem_identifier_reg_type":"JaLC"}]},"item_5_publisher_31":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"国立情報学研究所","subitem_publisher_language":"ja"}]},"item_5_source_id_32":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1346-5597","subitem_source_identifier_type":"ISSN"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"龍田, 真","creatorNameLang":"ja"},{"creatorName":"Tatsuta, Makoto","creatorNameLang":"en"}]},{"creatorNames":[{"creatorName":"藤田, 憲悦","creatorNameLang":"ja"},{"creatorName":"Fujita, Ken-etsu","creatorNameLang":"en"}]},{"creatorNames":[{"creatorName":"長谷川, 立","creatorNameLang":"ja"},{"creatorName":"Hasegawa, Ryu","creatorNameLang":"en"}]},{"creatorNames":[{"creatorName":"中野, 洋","creatorNameLang":"ja"},{"creatorName":"Nakano, Hiroshi","creatorNameLang":"en"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2019-03-12"}],"displaytype":"detail","filename":"08-005E.pdf","filesize":[{"value":"249.4 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment","url":"https://repository.nii.ac.jp/record/1243/files/08-005E.pdf"},"version_id":"96eabd21-27e1-4328-9582-dcb31f30becb"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"テクニカルレポート","subitem_subject_language":"ja","subitem_subject_scheme":"Other"},{"subitem_subject":"Technical Report","subitem_subject_language":"en","subitem_subject_scheme":"Other"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"departmental bulletin paper","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment","subitem_title_language":"en"}]},"item_type_id":"5","owner":"1","path":["136"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2019-03-12"},"publish_date":"2019-03-12","publish_status":"0","recid":"1243","relation_version_is_last":true,"title":["NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-05T08:32:22.013100+00:00"}