証明スコアによる問題モデルの検証技術

• 資料種別: 文書・図像類
• タイトル: 証明スコアによる問題モデルの検証技術
• 著者・編者: 二木, 厚吉
• 著者標目: 二木, 厚吉
• 出版年月日等: 2010-04-10
• 出版年（W3CDTF）: 2010-04-10
• 並列タイトル等: Verification of Problem Models with Proof Scores
• タイトル（掲載誌）: 科学研究費補助金研究成果報告書
• 掲載ページ: 1-4
• 本文の言語コード: jpn
• 件名標目: 仕様記述; 仕様検証; 形式手法; 問題モデル; 証明スコア; 帰納法; 場合分け
• 対象利用者: 一般
• 一般注記: 「帰納法」と「場合分け」は、問題モデル（問題領域や応用領域におけるモデル）の証明スコアによる検証法の基本技術である。本研究では、多様な応用分野で有効な帰納法と場合分けについて以下の成果を得た。(1) 帰納法をデータ型・プロセス型の帰納的な構造に基づき定式化した。(2) 場合分けを構成子からの項の生成に基づき定式化した。(3) (1),(2)に基づき、汎用的な証明規則を定式化するとともに、推論と探索を融合した強力な検証法を開発した。 : “Induction” and “case-splitting” are fundamentals of verifications of problem models (models in problem or application domains) by proof scores. The following research achievements are gotten about induction and case-splitting which are effective in many areas. (1) Induction is formalized based on recursive structures of data or process types. (2) Case-splitting is formalized based on generations of terms from generators. (3) Based on (1) and (2), universal proof rules are formalized, and a powerful verification method which harmonize inference and search is developed.; 研究種目：基盤研究（Ｂ）; 研究期間：2006～2009; 課題番号：18300008; 研究者番号： 50251971; 研究分野： 総合領域; 科研費の分科・細目： 情報学・ソフトウェア; identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/9034
• 記録形式（IMT）: application/pdf
• 一次資料へのリンクURL: https://dspace.jaist.ac.jp/dspace/bitstream/10119/9034/1/18300008seika.pdf
• オンライン閲覧公開範囲: 限定公開
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ