2024/04/27 更新

写真a

アオト　タカヒト
青戸 等人
Takahito Aoto
所属
教育研究院 自然科学系 情報電子工学系列 教授
工学部 工学科 教授
職名
教授
ホームページ
http://www.nue.ie.niigata-u.ac.jp/~aoto/index-j.html
外部リンク

学位

  • 博士(情報科学) （ 1997年3月   北陸先端科学技術大学院大学 ）

  • 学士(工学) （ 1992年3月   東京大学 ）

研究キーワード

  • ソフトウェア基礎

  • 定理自動証明

  • 書き換えシステム

研究分野

  • 情報通信 / 情報学基礎論

経歴（researchmap）

  • 新潟大学   工学部 工学科   教授

    2017年4月 - 現在

    　 詳細を見る

  • 新潟大学   工学部 情報工学科   教授

    2015年10月 - 2017年3月

    　 詳細を見る

  • 東北大学   電気通信研究所   准教授

    2007年4月 - 2015年9月

    　 詳細を見る

  • 東北大学   電気通信研究所   助教授

    2004年3月 - 2007年3月

    　 詳細を見る

  • 東北大学   電気通信研究所   講師

    2003年1月 - 2004年2月

    　 詳細を見る

  • 群馬大学   工学部   助手

    1998年3月 - 2002年12月

    　 詳細を見る

  • 北陸先端科学技術大学院大学   情報科学研究科   助手

    1997年4月 - 1998年2月

    　 詳細を見る

▶ 全件表示

経歴

  • 新潟大学   工学部　工学科   教授

    2017年4月 - 現在

  • 新潟大学   コンピュータサイエンス   教授

    2015年10月 - 2017年3月

学歴

  • 北陸先端科学技術大学院大学   情報科学研究科

    - 1997年3月

    　 詳細を見る

    国名： 日本国

    researchmap

  • 東京大学   工学部

    - 1992年3月

    　 詳細を見る

    国名： 日本国

    researchmap

所属学協会

委員歴

  • 11th International Workshop on Higher-Order Rewriting(HOR 2023)   プログラム委員  

    2023年   

    　 詳細を見る

  • 第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)   プログラム委員  

    2022年   

    　 詳細を見る

  • The 16th Logical and Semantic Frameworks with Applications (LSFA 2021)   プログラム委員  

    2021年   

    　 詳細を見る

  • The 13th International Symposium on Frontiers of Combining Systems(FroCoS 2021)   プログラム委員  

    2021年   

    　 詳細を見る

  • 10th International Joint Conference on Automated Reasoning (IJCAR 2020)   プログラム委員  

    2020年   

    　 詳細を見る

  • 28th International Conference on Computer Science Logic (CSL 2020)   プログラム委員  

    2020年   

    　 詳細を見る

  • The 33rd International Workshop on Unification (UNIF 2019)   プログラム委員  

    2019年   

    　 詳細を見る

  • International Workshop on Confluence   組織委員  

    2018年 - 2023年   

    　 詳細を見る

  • 7th Confluence Competition (CoCo 2018)・運営委員長  

    2018年   

    　 詳細を見る

  • 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)・プログラム委員  

    2018年   

    　 詳細を見る

  • ソフトウェア科学会   2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)・プログラム委員  

    2017年   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • 6th Confluence Competition (CoCo 2017)・運営委員長  

    2017年   

    　 詳細を見る

  • PPLサマースクール2017・幹事  

    2017年   

    　 詳細を見る

  • ソフトウェア科学会   プログラミング論研究会・運営委員  

    2016年4月 - 2020年3月   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016)・プログラム委員  

    2016年   

    　 詳細を見る

  • 8th International Workshop on Higher-Order Rewriting・プログラム委員  

    2016年   

    　 詳細を見る

  • 第18回プログラミングおよびプログラミング言語ワークショップ(PPL 2016)・プログラム共同委員長  

    2016年   

    　 詳細を見る

  • 5th Confluence Competition (CoCo 2016)・運営委員長  

    2016年   

    　 詳細を見る

  • IFIP WG1.6 on Rewriting   委員  

    2015年 - 現在   

    　 詳細を見る

  • 4th Confluence Competition (CoCo 2015)・運営委員長  

    2015年   

    　 詳細を見る

  • 第17回プログラミングおよびプログラミング言語ワークショップ(PPL 2015)・プログラム委員  

    2015年   

    　 詳細を見る

  • 10th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015)・プログラム委員  

    2015年   

    　 詳細を見る

  • 2d International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)・プログ ラム委員  

    2015年   

    　 詳細を見る

  • 4th International Workshop on Confluence (IWC 2015)・共同プログラム委員長  

    2015年   

    　 詳細を見る

  • 1st International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014)・プログラム委員  

    2014年   

    　 詳細を見る

  • 3rd Confluence Competition (CoCo 2014)・運営委員長  

    2014年   

    　 詳細を見る

  • 3rd International Workshop on Confluence (IWC 2014)・共同プログラム委員長  

    2014年   

    　 詳細を見る

  • Theoretical Computer Science特集号 New Directions in Rewriting・共同ゲストエディター  

    2012年   

    　 詳細を見る

  • 第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2012)・プログラム委員  

    2012年   

    　 詳細を見る

  • 1st Confluence Competition (CoCo 2012)・運営委員長  

    2012年   

    　 詳細を見る

  • 1st International Workshop on Confluence (IWC 2012)・プログラム委員  

    2012年   

    　 詳細を見る

  • 6th International Joint Conference on Automated Reasoning (IJCAR 2012)・プログラム委員  

    2012年   

    　 詳細を見る

  • Confluence Competition・運営委員  

    2011年 - 2018年7月   

    　 詳細を見る

  • 電子情報通信学会 英文論文誌ED分冊 フォーマルアプローチ特集・編集委員  

    2010年   

    　 詳細を見る

  • 21th International Conference on Rewriting Techniques and Applications (RTA 2010)・プログラム委員  

    2010年   

    　 詳細を見る

  • 情報処理学会   論文誌プログラミング・編集委員  

    2009年4月 - 2013年3月   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • 電子情報通信学会 英文論文誌ED分冊 フォーマルアプローチ特集・編集委員  

    2009年   

    　 詳細を見る

  • 第32回TRSミーティング・オーガナイザー(2009年)  

    2009年   

    　 詳細を見る

  • 20th International Conference on Rewriting Techniques and Applications (RTA 2009)・プログラム委員  

    2009年   

    　 詳細を見る

  • ソフトウェア科学会   第25回大会(2008年)・プログラム委員  

    2008年   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • 第10回プログラミングおよびプログラミング言語ワークショップ(PPL 2008)・実行委員長  

    2008年   

    　 詳細を見る

  • 情報処理学会   プログラミング研究会・運営委員  

    2007年4月 - 2011年3月   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • 第9回プログラミングおよびプログラミング言語ワークショップ(PPL 2007)・プログラム委員  

    2007年   

    　 詳細を見る

  • ソフトウェア科学会   第23回大会(2006年)・プログラム委員  

    2006年   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • ソフトウェア科学会   第22回大会(2005年)・プログラム委員  

    2005年   

    　 詳細を見る

    団体区分：学協会

    researchmap

  • 第16回TRSミーティング・オーガナイザー  

    2000年   

    　 詳細を見る

▶ 全件表示

 

論文

▶ 全件表示

MISC

  • 交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について 査読

    大野 峻, 青戸等人

    第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)   24   2022年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 置換に関する不動点制約を用いた名目書き換え 査読

    芳賀 雅樹, 青戸等人

    第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)   24   2022年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合 査読

    南山駿人, 青戸 人

    第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)   24   2022年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • A critical pair criterion for level-commutation of conditional term rewriting systems

    Ryota Haga, Yuki Kagaya, Takahito Aoto

    11th International Workshop on Confluence (IWC 2022)   2022年

    　詳細を見る

  • 危険対条件に基づく条件付き項書き換えシステムの階層可換性 査読

    芳賀亮太, 青戸等人

    第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)   24   2022年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 項書き換えシステムにおける局所十分完全性の証明法 査読

    白石智輝, 青戸 等人, 菊池 健太郎

    第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)   22   2020年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 条件付き項書き換えシステムの階層合流性証明法 査読

    加賀谷有輝, 青戸 等人

    第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)   22   2020年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 交換律による正則項書き換えにおける有限オートマトンの構成法とその応用 査読

    石塚守, 青戸 等人

    第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)   22   2020年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 決定手続きを用いた項書き換えシステムの帰納的定理自動証明 査読

    山口諒, 青戸 等人

    第21回プログラミングおよびプログラミング言語ワークショップ(PPL 2019)   21   2019年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 書き換え帰納法を利用した帰納的定理証明の補題生成法 査読

    加藤裕人, 青戸 等人

    第21回プログラミングおよびプログラミング言語ワークショップ(PPL 2019)   21   2019年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明 査読

    栗田泰智, 青戸 等人

    第20回プログラミングおよびプログラミング言語ワークショップ(PPL 2018)   20   2018年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • Ground confluence proof with pattern complementation

    Takahito Aoto, Yoshihito Toyama

    5th International Workshop on Confluence (IWC 2016)   2016年

    　詳細を見る

  • A rule-based procedure for equivariant nominal unification

    Takahito Aoto, Kentaro Kikuchi

    8th International Workshop on Higher-Order Rewriting (HOR 2016)   2016年

    　詳細を見る

  • 書き換え規則の重なりに基づく到達可能性判定法 査読

    島貫健太郎, 青戸 等人, 外山 芳人

    第17回プログラミングおよびプログラミング言語ワークショップ(PPL 2015)   17   2015年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 名目書き換えシステムの合流性について 査読

    鈴木貴樹, 菊池 健太郎, 青戸 等人, 外山 芳人

    第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)   16   2014年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 帰納的定理自動証明のための項書き換えシステム自動変換 査読

    佐藤洸一, 菊池 健太郎, 青戸 等人, 外山 芳人

    第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)   16   2014年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 閉包操作に基づく右基底項書き換えシステムの到達可能性判定 査読

    四方駿作, 青戸 等人, 外山 芳人

    第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)   16   2014年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 永続性と減少ダイアグラム法に基づく合流性自動証明 査読

    内田和真, 青戸 等人, 外山 芳人

    第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)   16   2014年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 書き換え帰納法に基づく帰納的定理の決定可能性 査読

    中嶋辰成, 青戸 等人, 外山 芳人

    第15回プログラミングおよびプログラミング言語ワークショップ(PPL 2013)   15   2013年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • ボトムアップ書き換えに基づく最内書き換え到達可能性判定 査読

    高橋翔大, 青戸 等人, 外山 芳人

    第15回プログラミングおよびプログラミング言語ワークショップ(PPL 2013)   15   2013年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 片側減少ダイアグラム法による項書き換えシステムの可換性証明法 査読

    的場正樹, 青戸 等人, 外山 芳人

    第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2012)   14   2012年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • Transformations by templates for simply-typed term rewriting

    Takahito Aoto, Yuki Chiba

    6th International Workshop on Higher-Order Rewriting (HOR 2012)   2012年

    　詳細を見る

  • 永続性にもとづく項書き換えシステムの合流性証明 査読

    鈴木翼, 青戸 等人, 外山 芳人

    第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2012)   14   2012年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 基底項書き換え系の多項式時間合流性判定法の改良 査読

    磯部耕己, 青戸等人, 外山芳人

    第13回プログラミングおよびプログラミング言語ワークショップ(PPL 2011)   13   2011年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 多項式サイズ正規形を保証する項書き換えシステムの経路順序 査読

    村井正勝, 青戸等人, 外山芳人

    第13回プログラミングおよびプログラミング言語ワークショップ(PPL 2011)   13   2011年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 無限項書き換えシステムにおける強頭部正規化可能性の反証手続き 査読

    岩見宗弘, 青戸 等人

    第12回プログラミングおよびプログラミング言語ワークショップ(PPL 2010)   12   2010年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 拡大手法に基づく項書き換え系の合流性自動証明 査読

    道又淳一, 青戸等人, 外山芳人

    第12回プログラミングおよびプログラミング言語ワークショップ(PPL 2010)   12   2010年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 項書き換えシステムの合流性判定, 査読

    吉田順一, 青戸 等人, 外山 芳人

    第10回プログラミングおよびプログラミング言語ワークショップ(PPL 2008)   10   2008年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • Designing a rewriting induction prover with an increased capability of non-orientable theorems

    Takahito Aoto

    Austrian-Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008)   2008年

    　詳細を見る

  • 反証機能付き書き換え帰納法のための補題自動生成法 査読

    嶌津聡志, 青戸 等人, 外山 芳人

    第10回プログラミングおよびプログラミング言語ワークショップ(PPL 2008)   10   2008年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • 項書き換えシステムの合流性自動判定 査読

    吉田順一, 青戸等人, 外山芳人

    情報技術レターズ   6   31 - 34   2007年

    　詳細を見る

  • 書き換え帰納法における向き付け不能な等式の証明 査読

    青戸 等人

    第8回プログラミングおよびプログラミング言語ワークショップ(PPL 2006)   8   2006年

    　詳細を見る

    記述言語：日本語  

    researchmap

  • パターンに基づくプログラム変換における列変数の導入 査読

    千葉勇輝, 青戸等人, 外山芳人

    情報技術レターズ   5 - 8   2005年

    　詳細を見る

  • Termination of simply-typed applicative term rewriting systems

    Takahito Aoto, Toshiyuki Yamada

    2nd International Workshop on Higher-Order Rewriting (HOR 2004)   2004年

    　詳細を見る

  • 高階関数型プログラムにおける帰納的定理証明 査読

    青戸等人, 山田俊行, 外山芳人

    情報技術レターズ   2   21 - 22   2003年

    　詳細を見る

▶ 全件表示

受賞

  • ソフトウェア科学会 研究論文賞

    2017年   ソフトウェア科学会   項書き換えシステムの変換を利用した帰納的定理自動証明

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    　詳細を見る

    受賞区分：国内学会・会議・シンポジウム等の賞  受賞国：日本国

    researchmap

  • 第12回プログラミングおよびプログラミング言語ワークショップ論文賞

    2012年3月   第12回プログラミングおよびプログラミング言語ワークショッププログラム委員会  

    鈴木翼, 青戸等人, 外山芳人

    　詳細を見る

    受賞区分：国内学会・会議・シンポジウム等の賞  受賞国：日本国

    researchmap

  • 第２回情報科学技術フォーラム論文賞

    2003年9月   情報処理学会  

    青戸等人, 山田俊行, 外山芳人

    　詳細を見る

    受賞区分：国内学会・会議・シンポジウム等の賞  受賞国：日本国

    researchmap

共同研究・競争的資金等の研究

  • 項書き換えシステムの解の一意性を保証する性質に関する研究

    研究課題/領域番号：21K11750

    2021年4月 - 2024年3月

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    青戸 等人

    　 詳細を見る

    配分額：4160000円 （ 直接経費：3200000円 、 間接経費：960000円 ）

    合流性(CR性)以外の解の一意性を保証する性質として，これまで研究されている性質には，正規形性(NFP性)，可換に関する一意正規形性(UNC性)，そして，簡約に関する一意正規形性(UNR性)の3つがある.これらの性質は，CR性⇒NFP性⇒UNC性⇒UNR性という論理関係がある.したがって，これらの3つの性質は合流性よりも弱い性質となっており，しかも，CR性，NFP性，UNC性，UNR性の順に階層を成している.本研究では，NFP性，UNC性，UNR性を始めとする，解の一意性を保証する，合流性より弱いさまざまな性質の検証理論や自動検証技術を開発する.
    右線形フラット項書き換えシステムにおけるUNR性の決定不能性の証明が文献(GodoyとJacquemardら(2009)によって与えられてる．しかし，その証明にはギャップがある．そこで，その証明の修正を試み，正しい証明を与えることに成功した．また，弱左線形項書き換えシステムにおいて，永続性を利用して，合流性を保証する理論が知られている．これはRnfが合流性を持つならばRが合流性を持つことを利用して，合流性条件を拡張している．類似の技法が，UNC性についても適用できないか検討した．このため，以下の性質を満たす項書き換えシステムを構築した：UNCの十分条件であるω-重なり性をもつが，重なり性をもたず，合流性ももたない．このような項書き換えシステムについて，そのUNCを検証する条件を発見できれば，実際にUNC性についても永続性を利用した検証手法が考案するのに役立つと考えられる．また，指向式条件付き項書き換えシステムのレベル可換性を保証する条件や局所十分完全性を保証する条件についても新しい条件を与えた．

    researchmap

  • 条件付き項書き換えシステムにおける帰納的定理と基底合流性に関する研究

    研究課題/領域番号：18K11158

    2018年4月 - 2022年3月

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    青戸 等人

    　 詳細を見る

    配分額：4420000円 （ 直接経費：3400000円 、 間接経費：1020000円 ）

    項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である.本研究では，指向式条件付き項書き換えシステムにおけるホーン節帰納的定理証明のための書き換え帰納法，指向式条件付き項書き換えシステムの基底合流性検証法，階層可換性の十分条件などを与えた．

    researchmap

  • 文脈移動変換と高階書き換え理論に基づくプログラム検証法の研究

    研究課題/領域番号：16K00091

    2016年4月 - 2019年3月

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    菊池 健太郎, 青戸 等人

    　 詳細を見る

    配分額：3510000円 （ 直接経費：2700000円 、 間接経費：810000円 ）

    書き換えシステムに基づく新しいプログラム検証手法を開発することを目的として研究を進めた。研究成果の概要は以下の通りである。
    (1) 束縛変数を伴う書き換えシステムに対して、名目書き換えシステムと関連する体系における合流性の判定条件についての成果が得られた。また、高階の書き換え体系に対する合流性・停止性の自動判定システムの開発に参加し、国際競技会において良い成績を収めた。
    (2) 文脈移動変換と関連する帰納的定理証明の手法に対して、十分完全性を持たない書き換えシステムにおける潜在帰納法についての考察から、無限リストのような計算が停止しない式を含むプログラムに適用可能な新しい検証手法を開発した。

    researchmap

  • 書き換えシステムの基底合流性自動証明の研究

    研究課題/領域番号：15K00003

    2015年4月 - 2018年3月

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    青戸 等人, 外山 芳人

    　 詳細を見る

    配分額：4550000円 （ 直接経費：3500000円 、 間接経費：1050000円 ）

    項書き換えシステムの基底合流性は，書き換えシステムに基づくソフトウェア検証法を構築する上で基礎となる性質である．本研究では，帰納的定理証明に用いられる書き換え帰納法に着目し，書き換え帰納法において束縛的変換可能性を保証すれば，基底合流性が成立することを示した．そして，束縛的変換可能性を保証する書き換え帰納法を設計して，その理論的な正当性の証明を与えた．また，書き換え規則の変換に基づく適切な関数定義の補完手法，順序付け不能な構成子規則を扱うための推論規則の拡張，基底合流性の反証法などの改良や拡張を考案した．そして，提案手法にもとづく基底合流性自動証明ツールAGCPを開発した．

    researchmap

  • 合流性に基づくプログラム自動検証法の研究

    研究課題/領域番号：25330004

    2013年4月 - 2016年3月

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    外山 芳人, 青戸 等人

    　 詳細を見る

    配分額：4550000円 （ 直接経費：3500000円 、 間接経費：1050000円 ）

    項書き換えシステムの理論は定理自動証明や計算モデルで広く利用されている。近年、項書き換えシステムの合流性自動証明システムがいくつか開発されているが、合流性自動証明システムの応用ついてはほとんど研究されていない。本研究では、項書き換えシステムの合流性自動証明システムに基づくプログラム自動検証法を研究する。研究成果としては、永続性と型情報に基づく合流性判定、プログラム変換に基づく定理自動証明、名目書き換えシステムの合流性条件、木オートマトン完備化の停止条件、基底合流性の自動判定、整礎順序をもつモノイド上の抽象リダクションシステムなどがある。

    researchmap

  • 定理自動証明における補題発見法に関する研究

    研究課題/領域番号：23500002

    2011年 - 2013年

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    青戸 等人, 外山 芳人

    　 詳細を見る

    配分額：5070000円 （ 直接経費：3900000円 、 間接経費：1170000円 ）

    書き換えシステムに基づく帰納的定理の自動証明における補題生成法について、補題候補の発見法や補題決定に有効な技術に資する成果を得た。主な研究成果としては、発散を生じる等式を解析するための基礎理論として、正則項の単一化および書き換え理論、半単一化についての理論について新しい知見を与えた。補題の決定手続きに適した書き換え帰納法の決定理論を拡張するとともに、書き換え帰納法において有効な補題決定手続きについて、始代数を用いるアプローチに基づく新しい手続きを考案した。また、書き換えシステムにおける末尾再帰を用いた関数定義において、自動証明に適した関数定義を得るための補題を抽出する手法を考案した。

    researchmap

  • 書き換えシステムの合流性自動判定法の研究

    研究課題/領域番号：22500002

    2010年 - 2012年

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    外山 芳人, 青戸 等人

    　 詳細を見る

    配分額：3640000円 （ 直接経費：2800000円 、 間接経費：840000円 ）

    項書き換えシステムの理論は定理自動証明や計算モデルでひろく利用されている。近年、項書き換えシステムの停止性自動証明システムが数多く開発されているにもかかわらず、合流性自動証明システムについてはほとんど研究されていない。本研究では、さまざまな手法に基いて項書き換えシステムの合流性自動証明システムACPを開発することである。研究成果としては、リダクション保存完備化による合流性自動証明、片側減少ダイアグラムによる可換性自動証明、多項式サイズ正規形を保証する経路順序、永続性をもちいた合流性自動証明などがある。合流性に関する国際ワークショップ(IWC2012)における合流性自動判定システムの第1回コンペティションにおいて、本研究で開発されたACPは、参加3システム中第1位の成績で優勝することができた。

    researchmap

  • リップリング法と書き換え帰納法を融合した定理自動証明法の研究

    研究課題/領域番号：20500002

    2008年 - 2010年

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    青戸 等人, 外山 芳人

    　 詳細を見る

    配分額：3640000円 （ 直接経費：2800000円 、 間接経費：840000円 ）

    プログラムの性質や仕様を記述する帰納的定理の自動証明法として項書き換えシステムに基づく暗黙的帰納法に着目し、その高度化を図った。主な研究成果としては、書き換え帰納法における順序付け不能な等式の取り扱いを改良するとともに、改良書き換え帰納法に基づく定理自動証明システムを構築した。また、帰納的定理自動証明に重要な補題自動生成法については、健全一般化法の一般化を行った。また、反証機能付き書き換え帰納法に対応する健全発散鑑定法を考案し、さらに、異なる複数の補題を独立に導入する書き換え帰納法フレームワークを考案した。複数の自動補題生成法を効率的に適用する戦略を構築した。また、反証機能付き書き換え帰納法の適用可能性に必要な合流性についてその証明法の理論を拡張するとともに、自動証明システムの構築を行った。

    researchmap

  • 定理自動証明に基づくプログラム変換システムの研究

    研究課題/領域番号：19500003

    2007年 - 2009年

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    外山 芳人, 青戸 等人

    　 詳細を見る

    配分額：3770000円 （ 直接経費：2900000円 、 間接経費：870000円 ）

    定理自動証明や計算モデルで広く利用されている項書き換えシステムの理論に基づいて、プログラム自動変換を実現するための基礎理論と実験システムを開発した。研究成果としては、プログラム変換のための変換パターン自動抽出アルゴリズムの提案と実験システムの構築、高階プログラムの新しい停止性証明法の提案、書き換え帰納法のための補題自動導入アルゴリズムの提案と実験システムの構築、分割統治法による項書き換えシステムの合流性自動判システムの開発を行った。

    researchmap

  • 高階関数を用いたプログラム検証および変換技術の高度化に関する研究

    研究課題/領域番号：17700002

    2005年 - 2007年

    制度名：科学研究費助成事業

    研究種目：若手研究(B)

    提供機関：日本学術振興会

    青戸 等人

    　 詳細を見る

    配分額：1700000円 （ 直接経費：1700000円 ）

    単純型付き項書き換えシステムの停止性検証手法の高度化を以下の点について試みた。(1)依存対手法における引数フィルタリングおよび使用可能規則を高階の場合への拡張を行った。(2)実験システムについての検討を進めた。特に、効率的な実装を実現するためのSAT検証器を用いた実装法についての検討を行い、その基本となる経路順序の符号化法について改良を行った。また停止性にもとづく帰納的定理の自動証明法である書き換え帰納法についての検討を進めた。特に反証付き書き換え帰納法に適した補題自動導入法について検討を行った。発散鑑定法を改良し、健全性を持つ発散鑑定法を提案した。実験システムを実装するとともに証明システムのベンチマークとなる例題集を抽出し、他の書き換え帰納法に基づく定理証明器との比較実験を行った。また、反証付き書き換え帰納法を利用するために必要な合流性を保障する方法について検討を進めた。停止性の検証器は多数提案されているのに対して、合流性の検証器の提案はあまりなされていないため、合流性の自動検証法について実験システムを構築し検討を行った。合流性の十分条件を満たさない項書き換えシステムについて分解手法を用いる判定法を利用することの検討を行い、分解手法を利用した合流性検証器の提案を行った。変換パターンに基づくプログラム変換のための変換パターンの抽出法について検討をすすめた。2階の一般化アルゴリズムを提案し、それに基づいて具体的なプログラム変換から変換パターンを抽出する実験を行った。変換に利用可能なパターンの抽出を容易にするためのヒューリスティクスについて検討を行い、いくつかの変換パターンの抽出に成功した。

    researchmap

  • 完備化に基づくプログラム自動変換の研究

    研究課題/領域番号：16016202

    2005年

    制度名：科学研究費助成事業

    研究種目：特定領域研究

    提供機関：日本学術振興会

    外山 芳人, 青戸 等人, 菊池 健太郎

    　 詳細を見る

    配分額：4500000円 （ 直接経費：4500000円 ）

    プログラム変換の手法である融合変換と、定理自動証明の手法である完備化を組み合わせた新しいプログラム変換手法を提案することを目的として、プログラム変換の実験と解析を行った。とくに、帰納的定理の強力な自動証明手法である書き換え帰納法と組み合わせることによって、プログラム変換に必要な性質を自動証明しながら、その結果を利用してプログラム変換を進めていくので、従来よりも強力な変換が可能となる。また、変換に必要な性質を自動的に発見することを可能とする補題発見機構を組み入れることにより、高度なプログラム自動変換を実現することができることを実証することができた。
    さらに、パターンをもちいたプログラム変換システムRAPTを開発した。これまでの研究から、プログラムの効率化にはいくつかの定石があることが明らかになっている。そこで、これらの定石を高階の変換パターンで表現し、パターンマッチングによるプログラム変換で効率を改良する方法を提案した。変換の正当性を検証するためには、プログラムのさまざまな帰納的性質を証明する必要がある。そこで、プログラムを書き換えシステムでモデル化し、定理自動証明の手法である潜在帰納法を適用することにより、プログラム変換とその正当性の検証を完全に自動化することに成功した。RAPTは入力プログラムを自動変換して出力プログラムを得るまでの手続きを6段階に分けて実現している。実装は関数型言語SMLをもちいて行い、ソースコードのサイズは約5000行である。
    また、プログラムの変換や検証に不可欠な基礎技術である高階プログラムの帰納的性質や停止条件に関する理論的な解析を進めるとともに、プログラムの実行メカニズムの設計に不可欠なリダクションの戦略に関する基礎理論の確立を行った。

    researchmap

  • 完備化に基づくプログラム自動変換の研究

    研究課題/領域番号：15017203

    2003年

    制度名：科学研究費助成事業

    研究種目：特定領域研究

    提供機関：日本学術振興会

    外山 芳人, 青戸 等人

    　 詳細を見る

    配分額：2100000円 （ 直接経費：2100000円 ）

    完備化に基づくプログラム融合変換のアイデアを,高階プログラムに適用するためには,高階書き換えシステムの完備化を実現する必要がある。しかし,高階書き換えシステムの完備化手続きの多くは机上の提案にとどまっており,実装にはいたっていない。これは,完備化手続きを実装するために不可欠な高階書き換えシステムの停止性が,簡単に判定できなかったからである。
    本研究では,項の幅の上界を設定することで,固定次数の関数記号に対する単純化順序の定義が,可変次数の関数記号に対してもそのまま有効に働くことに注目し,S式書き換えシステムの停止性が辞書式経路順序で簡単に判定できることを示した。実際に利用される高階書き換えシステムの多くは,S式書き換えシステムで表現できるため,ここで提案された停止性判定法をもちいて完備化可能である。我々は,S式書き換えシステムの完備化手続きを計算機上に実装し,高階書き換えシステムの完備化と融合変換が容易に実現できることを実験によって明らかにした。
    さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,高階関数を含む帰納的定理の自動証明法を検討し,高階書き換えシステムにおける潜在帰納法の枠組みを提案するとともに,潜在帰納法の適用に不可欠な十分完全性の判定が決定可能であることを明らかにした。
    また,書き換え代入に基づく2階のパターンマッチングを提案し,パターマッチングをもちいたプログラム変換手続きを改良するとともに,書き換え帰納法に基づく高階プログラムの融合変換の実験を行った。

    researchmap

  • リダクションの近似に基づくプログラム検証手法の研究

    研究課題/領域番号：14580357

    2002年 - 2005年

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    外山 芳人, 青戸 等人, 菊池 健太郎, 草刈 圭一郎

    　 詳細を見る

    配分額：2800000円 （ 直接経費：2800000円 ）

    リダクションの近似によるプログラム検証手法の基礎を確立する目的で、リダクションの正規化戦略、変換パターンに基づくプログラム等価変換、高階システムの停止性、高階帰納的定理の自動証明、到達可能性の決定可能性について研究し、理論解析と実験をとおして以下の成果を得た。
    (1)バランス弱合流性という概念に基づくリダクション戦略を提案した。左線形の項書き換えシステムの危険対が弱合流性をみたせば、外延リダクションが正規化戦略となることを明らかにした。これは、従来知られていた必須リダクションの正規化戦略を拡張しており、重なりのある項書き換えシステムに対しても適用可能である。また、正規保存近似によってリダクションを近似することで、外延リダクションが計算可能なリダクション戦略となることを示した。
    (2)変換パターンに基づく書き換えシステムの等価変換の理論を与え、それに基づくプログラム変換システムの提案を行った。ここで開発された手法は、潜在帰納法をもちいてデータ構造に基づくプログラムの帰納的性質を導いており、自動証明システムと組み合わせることで高度なプログラムの等価変換が可能となる。
    (3)書き換えシステムの正規化戦略の近似を理論的に解析し、従来知られていた強シーケンシャル近似、NV近似、右線形増加近似よりも強力な増加近似を提案した。この近似によって、これまでは困難であった広いクラスの書き換えシステムに対して正規化戦略を与えることが可能となった。さらに、増加近似が正規保存近似であることを利用して、書き換えシステムの合流性や停止性が決定可能となるクラスを明らかにした。

    researchmap

  • 宣言型プログラミング言語のためのAC記号のあるナローイングの計算理論

    研究課題/領域番号：14780187

    2002年 - 2004年

    制度名：科学研究費助成事業

    研究種目：若手研究(B)

    提供機関：日本学術振興会

    青戸 等人

    　 詳細を見る

    配分額：1100000円 （ 直接経費：1100000円 ）

    前年度に得られた高階項書き換え系における帰納的定理証明について解析を進めた.第1階の場合には自明に成立するが,高階では一般に成立しない帰納的定理の性質が単調性である.単調性を満たさないと高階帰納的定理の利用に様々な制約が課せられる.そこで,我々は,高階帰納的定理が単調性を持つための条件について考察した.まず,第1階項書き換え系における十分完全性の概念を拡張し,高階十分完全性の概念を与えた.そして,この概念を用いて,等式が単調高階帰納的定理となるための十分条件を明らかにした.次に,高階十分完全性の自動証明について考察を行なった.高階十分完全性の自動証明を行うため,初等性および高階図式という制約を導入し,高階十分完全性が決定可能となる単純型付き項書換え系のクラスを与えた.初等的な高階図式は多くの自然な高階関数プログラムを含む.以上の結果は,項書き換え分野の代表的な国際会議の1つであるRTA(書き換え技法と応用)'04に採録され,国際的な報告を行なった.
    前年度に得られた,単純型付き項書き換え系の停止性証明技法の実装について検討を行なった.その実装の第一段階として,より単純な体系である単純型付き適応的項書き換え系の停止性証明技法について考察を行なった.その過程で,適応的項書き換え系についてのみ適用可能な,非常に簡単で,しかも比較的強力な停止性証明技法を考案した.この成果は高階項書き換え系の国際ワークショップHOR'04に採録され,国際的な報告を行なった.

    researchmap

  • 理論計算機科学における数理論理学の応用

    研究課題/領域番号：08680356

    1996年 - 1997年

    制度名：科学研究費助成事業

    研究種目：基盤研究(C)

    提供機関：日本学術振興会

    小野 寛晰, 青戸 等人, 鹿島 亮, 石原 哉, 外山 芳人, WOLTER Frank, 酒井 正彦

    　 詳細を見る

    配分額：2400000円 （ 直接経費：2400000円 ）

    本研究の目標は、計算機科学に現われる数理論理学の問題を理論と応用の両面から解明しようとするものである。本年度に得られた成果のうちの主要なものを以下にあげる。
    1.代数的手法による縮約のない部分構造論理の一般論の展開(小野)
    2.部分構造論理におけるMaksimovaの変数分離の原理の研究(小野)
    3.直感主義的様相論理の研究(青戸、小野)
    4.項書き換え系における停止性および合流性に関する研究と関数型プログラム言語への応用(外山、青戸)
    5.弱い含意命題論理に対する証明論(鹿島)
    6.構成的数学の展開(石原)
    1)の縮約規則をもたない論理の一般論については、小野はその成果をポーランド、スウェーデン、スペイン、ドイツで発表した。また北陸先端科学技術大学院大学において、オーストラリアのM.Bunder博士、R.Gore博士およびアメリカのA.Scedrov教授とそれぞれ部分構造論理に関する共同研究をおこなった。2)については、いくつかの部分構造論理に対しMaksimovaの原理を証明論的手法により証明した。このようなアプローチはこの研究が始めてである。3)の直観主義様相論理については、青戸がその有限モデル性についての興味深い結果を示した。4)の項書き換え系とその応用については、外山と青戸が精力的に研究をおこない、優れた成果をおさめている。弱い含意論理におけるcut elimination theoremについては鹿島が、また構成的数学については石原がいくつかの成果をあげた。

    researchmap

▶ 全件表示

 

担当経験のある授業科目（researchmap）

  • リメディアル演習

    2022年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 総合工学概論

    2021年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • プログラミングAIII

    2019年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 工学リテラシー入門

    2017年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 知能情報システム概論

    2017年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 計算論理学

    2016年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 形式言語とオートマトン

    2016年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 数理論理学

    2016年
    -
    現在
    機関名：新潟大学

    　詳細を見る

  • 情報数理演習III

    2016年
    -
    2019年
    機関名：新潟大学

    　詳細を見る

  • 情報工学演習

    2016年
    -
    2018年
    機関名：新潟大学

    　詳細を見る

  • 情報工学基礎実習II

    2016年
    -
    2017年
    機関名：新潟大学

    　詳細を見る

  • 情報工学基礎実習I

    2016年
    -
    2017年
    機関名：新潟大学

    　詳細を見る

  • コンピュータへの招待

    2016年
    機関名：新潟大学

    　詳細を見る

▶ 全件表示

担当経験のある授業科目

  • リメディアル演習

    2022年
    -
    現在
    機関名：新潟大学

  • 総合工学概論

    2021年
    -
    現在
    機関名：新潟大学

  • 計算モデル特論

    2021年
    -
    現在
    機関名：新潟大学

  • 卒業研究

    2020年
    -
    2021年
    機関名：新潟大学

  • 研究室体験実習

    2020年
    機関名：新潟大学

  • 自然科学総論Ⅲ

    2020年
    機関名：新潟大学

  • プログラミングAIII

    2019年
    -
    現在
    機関名：新潟大学

  • 論文輪講

    2019年
    -
    2021年
    機関名：新潟大学

  • 卒業研修

    2019年
    -
    2020年
    機関名：新潟大学

  • 工学リテラシー入門(情報電子分野)

    2017年
    -
    現在
    機関名：新潟大学

  • 知能情報システム概論

    2017年
    -
    現在
    機関名：新潟大学

  • 計算論理学

    2016年
    -
    現在
    機関名：新潟大学

  • 形式言語とオートマトン

    2016年
    -
    現在
    機関名：新潟大学

  • 情報数理演習III

    2016年
    -
    2021年
    機関名：新潟大学

  • 情報工学基礎実習II

    2016年
    -
    2020年
    機関名：新潟大学

  • 情報工学基礎実習I

    2016年
    -
    2017年
    機関名：新潟大学

  • コンピュータへの招待

    2016年
    機関名：新潟大学

  • 技術英語入門

    2016年
    機関名：新潟大学

  • 数理論理学

    2015年
    -
    現在
    機関名：新潟大学

▶ 全件表示