| 研究成果の概要 |
組合せ数学, 論理と計算に関するセミナー等を中心に離散構造体に関する数学の形式化として, 有限オートマトン, スティッカー系, ファジー・データベースの定式化を行った. 研究集会「高信頼な理論と実装のための定理証明および定理証明器」では数学, 計算機科学, 産業界の各方面から, 国内外合わせて約80名の参加者が集い, 形式証明に関する結果の理解と今後の展開への道筋を共有することが出来た. また, 同時期に公開された400年来の難問であったケプラー予想の形式証明については, 解説記事を速報すると同時に, 数学教育現場に携わる先生方等への今後の数学の形式化についての傾向と展開について広報した.
|
