論証プログラミング

• Item type: Trans(1)
• 公開日: 1999-05-15
• タイトル: 論証プログラミング
• タイトル / 言語: en
• タイトル: Reasoning Programming
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: (株)富士通研究所パーソナルシステム研究所ネットメディア研究センター
• 著者所属: 九州大学システム情報科学研究科情報理学専攻
• 著者所属: 新潟大学工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Netmedia Laboratory, Fujitsu Laboratories Ltd.
• 著者所属(英): en
• 著者所属(英): Department of Informatics, Kyushu University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Niigata University
• 著者名: 南, 俊朗; 大谷, 武; 沢村, 一
• 著者名(英): Toshiro, Minami; Takeshi, Ohtani; Hajime, Sawamura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 論理的な問題解決の過程をプログラム実行と解釈することができる. 論理プログラミング言語Prologの場合Horn節集合にSLD導出を適用したResolution過程がプログラムの実行である. 一般の論理的問題解決支援システムにおいては一般の論理表現に 様々な証明戦略が適用される. 論証の全自動実行は困難であり人間との対話を通じた半自動的な実行となる. 本稿では Prologにおける論理プログラミングの枠を一般の論理系及び証明過程に拡張することにより 論証プログラミングという概念を提案する. 論証プログラミングにおいては 「プログラム」は導出規則で与えられ 「プログラムの実行」は証明戦略 (メタプログラム) に従った証明探索過程となる. 理論的に決定性の成り立つ論理系に対しても実際的証明のためには 人間と対話しつつ 証明戦略の構成とプログラムの実行が並行して行われる. 従って 論証プログラムは通常のプログラムの全自動実行とは異なり 利用者が介在した半自動実行もしくは手動実行となる. 論理プログラミングをこのような論証プログラミングに拡張することで 問題解決のための計算を一歩一歩進める手動実行から全自動実行までを統一的に扱うことができ また 対象世界のイメージを基に その形式的/論理モデルを構築する知識獲得のための過程と その対象世界における処理を行うプログラミング構成を連結して行うための基本的枠組みを与えることができる.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Logical problem solving processes can be interpreted as program executions. In the logic programming language Prolog, the program execution is the process of resolutions by applying the SLD-resolution to a set of Horn-clauses. In the general framework of logic-based problem solving, the general logical expressions are used and various proof strategies are applied on them. It is quite difficult to perform the reasoning fully automatically, thus the reasoning process goes with the user's intervention. In this paper, we propose the concept of "reasoning programming" by extending the framework of logic programming. In the reasoning programming, programs are given as the derivation rules and the program is executed in the proof searching process following to the proof strategies(or meta-programs) called tactics. Even in the theoretically decidable logics, the system will interact with humans for practical executions. Thus reasoning programming's executions normally go either semi-automatically or manually. By extending the concept of logic programming to reasoning programming, we can deal with calculations of problem solving from step-by-step executions to automatic executions in a unified framework. Further, we can give an elementary framework for connecting the process of knowledge acquisition from the human image of the target world to the construction of programs for processing in the world.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 40, 号 SIG04(PRO3), p. 77-77, 発行日 1999-05-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会