{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00033603","sets":["1164:2735:2790:2792"]},"path":["2792"],"owner":"1","recid":"33603","title":["一階論理表現の等価変換を用いた問題解決の正当性"],"pubdate":{"attribute_name":"公開日","attribute_value":"1999-09-21"},"_buckets":{"deposit":"d7677905-c0d9-4a34-a82c-2d8d4f9daaa2"},"_deposit":{"id":"33603","pid":{"type":"depid","value":"33603","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"一階論理表現の等価変換を用いた問題解決の正当性","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"一階論理表現の等価変換を用いた問題解決の正当性"},{"subitem_title":"The Correctness of Problem Solving using Equivalent Transformation of First - order Logical Expressions","subitem_title_language":"en"}]},"item_type_id":"4","publish_date":"1999-09-21","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"北海道大学大学院システム情報工学専攻"},{"subitem_text_value":"北海道大学情報メディア教育研究総合センター"},{"subitem_text_value":"北海道大学大学院システム情報工学専攻"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Division of System and Information Engineering, Hokkaido University","subitem_text_language":"en"},{"subitem_text_value":"Center of Infomation and Multimedia Studies, Hokkaido University","subitem_text_language":"en"},{"subitem_text_value":"Division of System and Information Engineering, Hokkaido University","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"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/33603/files/IPSJ-MPS99026012.pdf"},"date":[{"dateType":"Available","dateValue":"2001-09-21"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-MPS99026012.pdf","filesize":[{"value":"505.6 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"17"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"a02004c3-a6f7-4536-98dc-dff877b9b8e3","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 1999 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"吉田, 忠行"},{"creatorName":"赤間, 清"},{"creatorName":"宮本, 衛市"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Tadayuki, Yoshida","creatorNameLang":"en"},{"creatorName":"Kiyoshi, Akama","creatorNameLang":"en"},{"creatorName":"Eiichi, Miyamoto","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN10505667","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"論理プログラミングの理論では，当初は確定節で問題を表現していた．その後，否定の表現を取り入れ，さらには，否定を含む確定節を基礎として，一階述語論理の表現も確定節のボディで扱うことができるようになった．しかし論理プログラミングは，このような一階述語論理を含む確定節で表現されたプログラムを計算することに関して，正当性と柔軟性に問題を抱えている．本論文では，この問題を解決するために，等価変換パラダイムを採用する．等価変換の枠組で一階述語論理の表現を扱うために，一階論理制約の概念を導入する．一階論理制約とは，基本的な制約を論理記号によって組み立てた複合的な制約である．まず，一階論理制約の表現を定義し，その表現に対する意味を与える．そして，一階論理制約のための等価変換ルールを提案し，その正当性を証明する．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"In the theory of logic programming, the class of definite clauses was adopted first. Then the concept of logic programs was extended to include negative literals and arbitrary first-order formulas in the body of definite clauses. Computation of first-order expressions has, however, some difficulties with respect to the correctness and the flexibility. In this paper, the equivalent transformation paradigm (ET paradigm) is adopted to overcome these difficulties. We introduce first-order logical constraints, which are compound constraints composed of basic constraints constructed using logical connectives and quantifiers. We define the class of FLCs and determine the meaning of them. Next, we propose ET rules for FLCs and prove the correctness of these rules.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"48","bibliographic_titles":[{"bibliographic_title":"情報処理学会研究報告数理モデル化と問題解決（MPS）"}],"bibliographicPageStart":"45","bibliographicIssueDates":{"bibliographicIssueDate":"1999-09-21","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"76(1999-MPS-026)","bibliographicVolumeNumber":"1999"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"id":33603,"updated":"2025-01-22T15:37:21.542173+00:00","links":{},"created":"2025-01-18T23:02:24.108602+00:00"}