@article{oai:ipsj.ixsq.nii.ac.jp:00017017,
 author = {南, 俊朗 and 大谷, 武 and 沢村, 一 and Toshiro, Minami and Takeshi, Ohtani and Hajime, Sawamura},
 issue = {SIG04(PRO3)},
 journal = {情報処理学会論文誌プログラミング（PRO）},
 month = {May},
 note = {論理的な問題解決の過程をプログラム実行と解釈することができる. 論理プログラミング言語Prologの場合Horn節集合にSLD導出を適用したResolution過程がプログラムの実行である. 一般の論理的問題解決支援システムにおいては一般の論理表現に  様々な証明戦略が適用される. 論証の全自動実行は困難であり人間との対話を通じた半自動的な実行となる. 本稿では  Prologにおける論理プログラミングの枠を一般の論理系及び証明過程に拡張することにより  論証プログラミングという概念を提案する. 論証プログラミングにおいては  「プログラム」は導出規則で与えられ  「プログラムの実行」は証明戦略 (メタプログラム) に従った証明探索過程となる. 理論的に決定性の成り立つ論理系に対しても実際的証明のためには  人間と対話しつつ  証明戦略の構成とプログラムの実行が並行して行われる. 従って  論証プログラムは通常のプログラムの全自動実行とは異なり  利用者が介在した半自動実行もしくは手動実行となる. 論理プログラミングをこのような論証プログラミングに拡張することで  問題解決のための計算を一歩一歩進める手動実行から全自動実行までを統一的に扱うことができ  また  対象世界のイメージを基に  その形式的/論理モデルを構築する知識獲得のための過程と  その対象世界における処理を行うプログラミング構成を連結して行うための基本的枠組みを与えることができる., 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.},
 pages = {77--77},
 title = {論証プログラミング},
 volume = {40},
 year = {1999}
}