Reasoning with Conditional Probabilities and Joint Distributions in Coq

• 資料種別: 記事
• タイトル: Reasoning with Conditional Probabilities and Joint Distributions in Coq
• 著者・編者: Reynald Affeldt; Jacques Garrigue; 才川 隆文
• 著者標目: Reynald Affeldt; Jacques Garrigue; 才川 隆文
• 並列タイトル等: Coqによる条件付き確率と同時分布の形式化とその応用 Coq ニ ヨル ジョウケン ツキ カクリツ ト ドウジ ブンプ ノ ケイシキカ ト ソノ オウヨウ
• タイトル（掲載誌）: コンピュータソフトウェア = Computer software / 日本ソフトウェア科学会 編
• 巻号年月日等（掲載誌）: 37(3):2020.8
• 掲載巻: 37
• 掲載号: 3
• 掲載ページ: 79-95
• 掲載年月日（W3CDTF）: 2020-08
• ISSN（掲載誌）: 0289-6540
• ISSN-L（掲載誌）: 0289-6540
• 出版事項（掲載誌）: 東京 : 日本ソフトウェア科学会 ; 1984-
• 出版地（国名コード）: JP
• 本文の言語コード: eng
• NDLC: ZM13
• 対象利用者: 一般
• 所蔵機関: 国立国会図書館
• 請求記号: Z14-1033
• 連携機関・データベース: 国立国会図書館 : 国立国会図書館雑誌記事索引; https://ndlsearch.ndl.go.jp
• 書誌ID（NDLBibID）: 030585163; http://id.ndl.go.jp/bib/030585163
• 整理区分コード: 632

• 要約等: <p>Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations. Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize. In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of probabilistic graphical models.</p>
• DOI: 10.11309/jssst.37.3_79
• オンライン閲覧公開範囲: インターネット公開
• 連携機関・データベース: 科学技術振興機構 : J-STAGE; http://www.jstage.jst.go.jp

• 要約等: <p>Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations. Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize. In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of probabilistic graphical models.</p>
• DOI: 10.11309/jssst.37.3_79; https://doi.org/10.11309/jssst.37.3_79
• オンライン閲覧公開範囲: インターネット公開
• 関連情報（URI）: http://id.ndl.go.jp/bib/030585163; https://ndlsearch.ndl.go.jp/books/R000000004-I030585163
• 連携機関・データベース: 国立情報学研究所 : CiNii Research; https://cir.nii.ac.jp/
• 提供元機関・データベース: Japan Link Center; https://japanlinkcenter.org/top; 雑誌記事索引データベース; https://ndlsearch.ndl.go.jp; CiNii Articles; 科学研究費助成事業データベース; https://kaken.nii.ac.jp/ja
• 書誌ID（NDLBibID）: 030585163; http://id.ndl.go.jp/bib/030585163
• NII論文ID: 130007906562; 40022319106