{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00014318","sets":["581:768:780"]},"path":["780"],"owner":"1","recid":"14318","title":["プログラム生成システムPAPYRUS"],"pubdate":{"attribute_name":"公開日","attribute_value":"1994-01-15"},"_buckets":{"deposit":"6c5d4e09-b73b-42c4-9eb8-021661bd9096"},"_deposit":{"id":"14318","pid":{"type":"depid","value":"14318","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"プログラム生成システムPAPYRUS","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"プログラム生成システムPAPYRUS"},{"subitem_title":"PAPYRUS : A System for Program Synthesis and Verification by Constructive Logics","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"論文","subitem_subject_scheme":"Other"}]},"item_type_id":"2","publish_date":"1994-01-15","item_2_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"（財）新世代コンピュータ技術開発機構／現在　（株）東芝システム・ソフトウェア生産技術研究所"},{"subitem_text_value":"筑波大学電子・情報工学系"},{"subitem_text_value":"（株）三菱総合研究所"},{"subitem_text_value":"（財）新世代コンピュータ技術開発機構"},{"subitem_text_value":"（株）ヴァンリッチ／現在　にっかつ芸術学院映像科"}]},"item_2_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Institute for New Generation Computer Technology/Presently with System and Software Engineering Laboratoriy, Toshiba Co., Ltd","subitem_text_language":"en"},{"subitem_text_value":"Institute of Information Science and Electronics, University of Tsukuba","subitem_text_language":"en"},{"subitem_text_value":"Mitsubishi Research Institute, Inc.","subitem_text_language":"en"},{"subitem_text_value":"VanRich Corporation","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/14318/files/IPSJ-JNL3501012.pdf"},"date":[{"dateType":"Available","dateValue":"1996-01-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL3501012.pdf","filesize":[{"value":"1.4 MB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"8"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"987914e3-3df1-4feb-b211-43997692619d","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 1994 by the Information Processing Society of Japan"}]},"item_2_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"川田, 秀司"},{"creatorName":"坂井, 公"},{"creatorName":"藤田, 正幸"},{"creatorName":"白井, 康之"},{"creatorName":"大坪透"}],"nameIdentifiers":[{}]}]},"item_2_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Hideji, Kawata","creatorNameLang":"en"},{"creatorName":"Ko, Sakai","creatorNameLang":"en"},{"creatorName":"Masayuki, Fujita","creatorNameLang":"en"},{"creatorName":"Yasuyuki, Shirai","creatorNameLang":"en"},{"creatorName":"Toru, Ohtubo","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_2_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN00116647","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_2_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7764","subitem_source_identifier_type":"ISSN"}]},"item_2_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"Curry-Howard Isomorphismに墓づくプログラム生成法では、諭理式に対しプログラムの仕様としての解釈を定義し、諭理式の証明から誤りのないプログラムの生成方式をあたえる。PAPYRUS（PArallel Programs sYnthesis by Reasoning Upon System）は、このような方法をべ一スとしたプログラム生成実験システムであり、大まかには以下の2つの機能を提供する。1つは、諭理や表記法、プログラム生成規則の管理と、これらの定義のもとでの証明チェックやプログラム生成の機能で、型諭理の1つであるCC（Calculus of Constructions）における型推諭機能とTRS（Term Rewriting System）の技術により実現される、これらの定議を変更することにより、プログラム生成のためのさまざまな諭理や表現方法、実現可能性解釈を利用することがで妻る。もう1つは、証明作成の簡単化を目的とする証明エディタ機能であり、（1）適用可能な推論規測の表示と、選択された規則による自動証明展開機能、（2）部分証明が構成されるたびに行われる自動証明チェック機能（この機能により完成した証明はその時点で正しさが保証される）、（3）未証明部をプルーバに証明させる機能などがある。本稿ではPAPYRUSの原理と構成、機能について述ぺる。","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"142","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicPageStart":"127","bibliographicIssueDates":{"bibliographicIssueDate":"1994-01-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"1","bibliographicVolumeNumber":"35"}]},"relation_version_is_last":true,"item_2_alternative_title_2":{"attribute_name":"その他タイトル","attribute_value_mlt":[{"subitem_alternative_title":"ソフトウェア工学"}]},"weko_creator_id":"1"},"id":14318,"updated":"2025-01-23T00:51:49.679272+00:00","links":{},"created":"2025-01-18T22:48:09.988443+00:00"}