Group structure of n-way contingency tables with a proof assistant system

• Project/Area Number: 19700269
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Statistical science
• Research Institution: Niigata University of International and Information Studies
• Principal Investigator: ONO Yoko Niigata University of International and Information Studies, 情報文化学部, 講師 (60339140)
• Project Period (FY): 2007 – 2008
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥3,390,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥390,000); Fiscal Year 2008: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000); Fiscal Year 2007: ¥1,700,000 (Direct Cost: ¥1,700,000)
• Keywords: 計算機集約的統計 / 汎用証明支援システム / 形式化手法 / 半自動証明 / 分割表 / Isabelle / 数え上げ / 半自動化 / 直観証明 / 群論

Research Abstract

本研究の目的は、対話型汎用証明支援システムであるIsabelleを用い、群構造を考慮した多次元分割表の性質を明らかにすることである。特に、これまでに蓄積されている群論等の証明成功過程ライブラリを知識として用い、分割表の数え上げに関する問題を群の問題として置き直した命題を作成し、この命題を計算機上でIsabelleを用いて証明を行った。この証明とは、計算機を集中的に酷使する全列挙的なものではなく、論理構造を辿るものである。

Research Products

• [Journal Article] Comparison a human proof in Isabelle (2008)
  • Author(s): Yoko Ono and Hidetsune Kobayashi
  • Journal Title: Proceedings of the 2nd Workshop on Programming Languages for Mechanized Mathematical Systems
  • Peer Reviewed
• [Journal Article] Comparison a human proof with a proof in Isabelle (2008)
  • Author(s): Yoko Ono and Hidetsune Kobayashi
  • Journal Title: Proc. of the 2^<nd> Workshop on Programming Languages for Mechanized Mathematics Systems Pages: 29-40
  • Peer Reviewed
• [Presentation] 分割表上のメトロポリスウォークの数値精度改良 (2008)
  • Author(s): 橋口博樹,小野陽子,黒田正博
  • Organizer: 第22回日本計算機統計学会
  • Place of Presentation: (財)先端医療振興財団・臨床研究情報センター(兵庫県神戸市)
  • Year and Date: 2008-11-06
• [Presentation] A Proof by Automated Reasoning (2008)
  • Author(s): H. Kobayashi, Z. Zeng and Y. Ono
  • Organizer: Computers in Scientific Discovery 4
  • Place of Presentation: Shanghai, China
  • Year and Date: 2008-03-30
• [Presentation] A Trial for Automated Proof (2008)
  • Author(s): Hidetsune Kobayashi, Zhenbing Zeng and Yoko Ono
  • Organizer: Computers in Scientific Discovery 4
  • Place of Presentation: East China Normal University, Shanghai, China
  • Year and Date: 2008-03-28
• [Presentation] On Comparison of p-values for Contingency Tables between MCMC and Direct Sampling (2007)
  • Author(s): Yoko Ono and Hiroki Hashiguchi
  • Organizer: Bulletin of the 56rd Session of the International Statistical Institute
  • Place of Presentation: Lisbon, Portugal
  • Year and Date: 2007-08-28
• [Presentation] On Comparison of p-values for Contingency Tables between MCMC and Direct Sampling (2007)
  • Author(s): Y. Ono and H. Hashiguchi
  • Organizer: ISI 56th
  • Place of Presentation: Lisboa, Portugal
  • Year and Date: 2007-08-28