2016 年度研究成果報告書

定理証明支援系による形式木言語理論の定式化

研究課題

研究課題/領域番号	25730002
研究種目	若手研究(B)
配分区分	基金
研究分野	情報学基礎理論
研究機関	電気通信大学
研究代表者	中野圭介電気通信大学, 大学院情報理工学研究科, 准教授 (30505839)
研究期間 (年度)	2013-04-01 – 2017-03-31
キーワード	形式言語理論 / 定理証明支援系 / 木トランスデューサ
研究成果の概要	木構造データから木構造データへ変換するモデルである木トランスデューサ理論は，プログラミング言語理論やデータベース理論において重要な役割を果たしており，1960年代から盛んに研究が行われている．本研究の目的は，この理論を計算機の上で定式化し，その中の定理に対して機械的に検査可能な形の厳密な証明を与えることである．この成果により，今後の同分野の着実な発展が期待され，さらに堅牢なソフトウェア開発への応用の基盤を提供することが可能となる．
自由記述の分野	情報学基礎