Updated on 2024/04/24
博士(情報科学) ( 1997.3 北陸先端科学技術大学院大学 )
学士(工学) ( 1992.3 東京大学 )
Foundations of Software
Automated Theorem Proving
Term Rewriting
Informatics / Theory of informatics
Niigata University Faculty of Engineering Department of Engineering Professor
2017.4
Niigata University Faculty of Engineering Department of Information Engineering Professor
2015.10 - 2017.3
Tohoku University Research Institute of Electrical Communication Associate Professor
2007.4 - 2015.9
Tohoku University Research Institute of Electrical Communication Associate Professor (as old post name)
2004.3 - 2007.3
Tohoku University Research Institute of Electrical Communication Lecturer
2003.1 - 2004.2
Gunma University Faculty of Engineering Research Assistant
1998.3 - 2002.12
Japan Advanced Institute of Science and Technology School of Information Science Research Assistant
1997.4 - 1998.2
Niigata University Faculty of Engineering Department of Engineering Professor
2017.4
Niigata University Abolition organization Computer Science Professor
2015.10 - 2017.3
Japan Advanced Institute of Science and Technology Graduate School, Division of Information Science
- 1997.3
Country： Japan
The University of Tokyo Faculty of Engineering
- 1992.3
Country： Japan
IPSJプログラミング研究会
ACM
ソフトウェア科学会
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
Committee type：Academic society
6th Confluence Competition (CoCo 2017)・運営委員長
2017
PPLサマースクール2017・幹事
2017
ソフトウェア科学会 プログラミング論研究会・運営委員
2016.4 - 2020.3
Committee type：Academic society
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
Committee type：Academic society
電子情報通信学会 英文論文誌ED分冊 フォーマルアプローチ特集・編集委員
2009
第32回TRSミーティング・オーガナイザー(2009年)
2009
20th International Conference on Rewriting Techniques and Applications (RTA 2009)・プログラム委員
2009
ソフトウェア科学会 第25回大会(2008年)・プログラム委員
2008
Committee type：Academic society
第10回プログラミングおよびプログラミング言語ワークショップ(PPL 2008)・実行委員長
2008
情報処理学会 プログラミング研究会・運営委員
2007.4 - 2011.3
Committee type：Academic society
第9回プログラミングおよびプログラミング言語ワークショップ(PPL 2007)・プログラム委員
2007
ソフトウェア科学会 第23回大会(2006年)・プログラム委員
2006
Committee type：Academic society
ソフトウェア科学会 第22回大会(2005年)・プログラム委員
2005
Committee type：Academic society
第16回TRSミーティング・オーガナイザー
2000
Yuki Sato, Takahito Aoto
IPSJ Transactions on Programming 14 ( 2 ) 15 - 24 2021
Commutative Rational Term Rewriting. Reviewed
Mamoru Ishizuka, Takahito Aoto, Munehiro Iwami
Language and Automata Theory and Applications - 15th International Conference(LATA) 200 - 212 2021
A Proof Method for Local Sufficient Completeness of Term Rewriting Systems. Reviewed
Tomoki Shiraishi, Kentaro Kikuchi, Takahito Aoto
Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium(ICTAC) 386 - 404 2021
Kentaro Kikuchi, Takahito Aoto
41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science(FSTTCS) 49 - 15 2021
A Category-theoretic Formalization of Unification over Rational Terms Reviewed
Kairi Miyamae, Takahito Aoto
IPSJ Transactions on Programming 14 ( 2 ) 1 - 14 2021
Masaomi Yamaguchi, Takahito Aoto
5th International Conference on Formal Structures for Computation and Deduction(FSCD) 11 - 23 2020
Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. Reviewed
Kentaro Kikuchi, Takahito Aoto
Logic-Based Program Synthesis and Transformation - 30th International Symposium(LOPSTR) 56 - 73 2020
Formalizing Rewriting Induction on Isabelle/HOL Reviewed
KIMURA Yuta, AOTO Takahito
Computer Software 37 ( 2 ) 2_104 - 2_119 2020
Automated Proofs of Horn-Clause Inductive Theo- rems for Conditional Term Rewriting Systems. Reviewed
Taichi Kurita, Takahito Aoto
Computer Software 36 ( 2 ) 61 - 75 2019
Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems. Reviewed
Takahito Aoto, Yoshihito Toyama
Frontiers of Combining Systems - 12th International Symposium(FroCos) 330 - 347 2019
Kentaro Kikuchi, Takahito Aoto, Isao Sasano
Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages(PPDP) 13 - 14 2019
Confluence Competition 2018. Reviewed
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, Harald Zankl
3rd International Conference on Formal Structures for Computation and Deduction(FSCD) 32 - 5 2018
Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems. Reviewed
Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama
Frontiers of Combining Systems - 11th International Symposium(FroCoS) 115 - 131 2017
Improving Rewriting Induction Approach for Proving Ground Confluence. Reviewed
Takahito Aoto, Yoshihito Toyama, Yuta Kimura
2nd International Conference on Formal Structures for Computation and Deduction(FSCD) 7 - 18 2017
Nominal Confluence Tool. Reviewed
Takahito Aoto, Kentaro Kikuchi
Automated Reasoning - 8th International Joint Conference(IJCAR) 173 - 182 2016
Critical Pair Analysis in Nominal Rewriting. Reviewed
Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama
7th International Symposium on Symbolic Computation in Software Science(SCSS) 156 - 168 2016
Ground Confluence Prover based on Rewriting Induction. Reviewed
Takahito Aoto, Yoshihito Toyama
1st International Conference on Formal Structures for Computation and Deduction(FSCD) 33 - 12 2016
Decision Method of Reachability Based on Rewrite Rule Overlapping. Reviewed
Kentaro Shimanuki, Takahito Aoto, Yoshihito Toyama
Computer Software 33 ( 3 ) 93 - 107 2016
Automated Inductive Theorem Proving Using Transformations of Term Rewriting Systems. Reviewed
Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama
Computer Software 32 ( 1 ) 179 - 193 2015
Confluence of Orthogonal Nominal Rewriting Systems Revisited. Reviewed
Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama
26th International Conference on Rewriting Techniques and Applications(RTA) 301 - 317 2015
Correctness of Context-Moving Transformations for Term Rewriting Systems. Reviewed
Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama
Logic-Based Program Synthesis and Transformation - 25th International Symposium(LOPSTR) 331 - 345 2015
Confluence Competition 2015. Reviewed
Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, Harald Zankl
Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction(CADE) 101 - 104 2015
Innermost Reachability of Bottom-Up Innermost Term Rewriting Systems. Reviewed
Shota Takahashi, Takahito Aoto, Yoshihito Toyama
Computer Software 31 ( 1 ) 75 - 89 2014
Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams. Reviewed
Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida
Rewriting and Typed Lambda Calculi - Joint International Conference(RTA-TLCA) 46 - 60 2014
Decision Procedures for Proving Inductive Theorems without Induction. Reviewed
Takahito Aoto, Sorin Stratulat
Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming(PPDP) 237 - 248 2014
Decidability of Inductive Theorems Based on Rewriting Induction. Reviewed
Tatsunari Nakazima, Takahito Aoto, Yoshihito Toyama
Computer Software 31 ( 3 ) 294 - 306 2014
Commutativity of Term Rewriting Systems Based on One Side Decreasing Diagrams. Reviewed
Masaki Matoba, Takahito Aoto, Yoshihito Toyama
Computer Software 30 ( 1 ) 187 - 202 2013
Termination of Rule-Based Calculi for Uniform Semi-Unification. Reviewed
Takahito Aoto, Munehiro Iwami
Language and Automata Theory and Applications - 7th International Conference(LATA) 56 - 67 2013
Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering. Reviewed
Takahito Aoto
Frontiers of Combining Systems - 9th International Symposium(FroCos) 311 - 326 2013
Confluence Proofs of Term Rewriting Systems Based on Persistency Reviewed
Tsubasa Suzuki, Takahito Aoto, Yoshihito Toyama
Computer Software 30 ( 3 ) 148 - 162 2013
Disproving Strong Head Normalization and General Productivity Automatically in Infinitary Term Rewriting Systems. Reviewed
Munehiro Iwami, Takahito Aoto
Computer Software 29 ( 1 ) 211 - 239 2012
Rational Term Rewriting Revisited: Decidability and Confluence. Reviewed
Takahito Aoto, Jeroen Ketema
Graph Transformations - 6th International Conference(ICGT) 172 - 186 2012
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems Reviewed
Takahito Aoto, Yoshihito Toyama
Logical Methods in Computer Science 8 ( 1 ) 2012
A Path Ordering for Term Rewriting Systems with Polynomial Size Normal Forms. Reviewed
Kouki Isobe, Takahito Aoto, Yoshihito Toyama
Computer Software 29 ( 1 ) 176 - 190 2012
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems. Reviewed
Takahito Aoto, Yoshihito Toyama
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications(RTA) 91 - 106 2011
Natural Inductive Theorems for Higher-Order Rewriting. Reviewed
Takahito Aoto, Toshiyuki Yamada, Yuki Chiba
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications(RTA) 107 - 121 2011
Program Transformation Templates for Tupling Based on Term Rewriting. Reviewed
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
IEICE Transactions on Information & Systems 93-D ( 5 ) 963 - 973 2010
Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling. Reviewed
Takahito Aoto
Proceedings of the 21st International Conference on Rewriting Techniques and Applications(RTA) 7 - 16 2010
Automated Lemma Generation for Rewriting Induction with Disproof. Reviewed
Satoshi Shimazu, Takahito Aoto, Yoshihito Toyama
Computer Software 26 ( 2 ) 41 - 55 2009
Proving Confluence of Term Rewriting Systems Automatically. Reviewed
Takahito Aoto, Junichi Yoshida, Yoshihito Toyama
Rewriting Techniques and Applications(RTA) 93 - 102 2009
Argument Filterings and Usable Rules for Simply Typed Dependency Pairs. Reviewed
Takahito Aoto, Toshiyuki Yamada
Frontiers of Combining Systems(FroCoS) 117 - 132 2009
Automating Confluence Check of Term Rewriting Systems. Reviewed
Junichi Yoshida, Takahito Aoto, Yoshihito Toyama
Computer Software 26 ( 2 ) 76 - 92 2009
Soundness of Rewriting Induction Based on an Abstract Principle Reviewed
Takahito Aoto
IPSJ Transactions on Programming 49 ( SIG 1 ) 28 - 38 2008
Sound Lemma Generation for Proving Inductive Validity of Equations. Reviewed
Takahito Aoto
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science(FSTTCS) 13 - 24 2008
Automatic Construction of Program Transformation Templates. Reviewed
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
IPSJ Transactions on Programming 49 ( SIG 1 (PRO 35) ) 14 - 27 2008
Program Transformation by Templates: A Rewriting Framework. Reviewed
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
IPSJ Transactions on Programming 47 52 - 65 2006
RAPT: A Program Transformation System Based on Term Rewriting. Reviewed
Yuki Chiba, Takahito Aoto
Term Rewriting and Applications(RTA) 267 - 276 2006
Dealing with Non-orientable Equations in Rewriting Induction. Reviewed
Takahito Aoto
Term Rewriting and Applications(RTA) 242 - 256 2006
Program transformation by templates based on term rewriting. Reviewed
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP) 59 - 69 2005
Dependency Pairs for Simply Typed Term Rewriting. Reviewed
Takahito Aoto, Toshiyuki Yamada
Term Rewriting and Applications(RTA) 120 - 134 2005
Inductive Theorems for Higher-Order Rewriting. Reviewed
Takahito Aoto, Toshiyuki Yamada, Yoshihito Toyama
Rewriting Techniques and Applications(RTA) 269 - 284 2004
Proving Termination of Simply Typed Term Rewriting Systems Automatically. Reviewed
Takahito Aoto, Toshiyuki Yamada
IPSJ Transactions on Programming 44 ( SIG 4 (PRO 17) ) 67 - 77 2003
Termination of Simply Typed Term Rewriting by Translation and Labelling. Reviewed
Takahito Aoto, Toshiyuki Yamada
Rewriting Techniques and Applications(RTA) 380 - 394 2003
Solution to the Problem of Zantema on a Persistent Property of Term Rewriting Systems. Reviewed
Takahito Aoto
Journal of Functional and Logic Programming 2001 ( 11 ) 2001
Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Reviewed
Takahito Aoto
Journal of Logic, Language and Information 8 ( 2 ) 217 - 242 1999
On the Finite Model Property of Intuitionistic Modal Logics over MIPC. Reviewed
Takahito Aoto, Hiroyuki Shirasu
Mathematical Logic Quarterly 45 435 - 448 1999
Termination Transformation by Tree Lifting Ordering. Reviewed
Takahito Aoto, Yoshihito Toyama
Rewriting Techniques and Applications(RTA) 256 - 270 1998
Solution to the Problem of Zantema on a Persistent Property of Term Rewriting Systems. Reviewed
Takahito Aoto
Principles of Declarative Programming(PLILP/ALP) 250 - 265 1998
Some Characterizations of Implicational Formulas in the Intuitionistic Logic.
Takahito Aoto
1997
On Composable Properties of Term Rewriting Systems. Reviewed
Takahito Aoto, Yoshihito Toyama
Algebraic and Logic Programming(ALP/HOA) 114 - 128 1997
Persistency of Confluence. Reviewed
Takahito Aoto, Yoshihito Toyama
Journal of Universal Computer Science 3 ( 11 ) 1134 - 1147 1997
Non-Uniqueness of Normal Proofs for Minimal Formulas in Implication-Conjunction Fragment of BCK. Reviewed
Takahito Aoto, Hiroakira Ono
Bulletin of the Section of Logic 23 ( 3 ) 104 - 112 1994
交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について Reviewed
The 24th JSSST Workshop on Programming and Programming Languages(PPL 2022) 24 2022
置換に関する不動点制約を用いた名目書き換え Reviewed
The 24th JSSST Workshop on Programming and Programming Languages(PPL 2022) 24 2022
書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合 Reviewed
The 24th JSSST Workshop on Programming and Programming Languages(PPL 2022) 24 2022
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
危険対条件に基づく条件付き項書き換えシステムの階層可換性 Reviewed
The 24th JSSST Workshop on Programming and Programming Languages(PPL 2022) 24 2022
項書き換えシステムにおける局所十分完全性の証明法 Reviewed
The 22nd JSSST Workshop on Programming and Programming Languages(PPL 2020) 22 2020
条件付き項書き換えシステムの階層合流性証明法 Reviewed
The 22nd JSSST Workshop on Programming and Programming Languages(PPL 2020) 22 2020
交換律による正則項書き換えにおける有限オートマトンの構成法とその応用 Reviewed
The 22nd JSSST Workshop on Programming and Programming Languages(PPL 2020) 22 2020
決定手続きを用いた項書き換えシステムの帰納的定理自動証明 Reviewed
The 21st JSSST Workshop on Programming and Programming Languages(PPL 2019) 21 2019
書き換え帰納法を利用した帰納的定理証明の補題生成法 Reviewed
The 21st JSSST Workshop on Programming and Programming Languages(PPL 2019) 21 2019
条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明 Reviewed
The 20th JSSST Workshop on Programming and Programming Languages(PPL 2018) 20 2018
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
書き換え規則の重なりに基づく到達可能性判定法 Reviewed
The 17th JSSST Workshop on Programming and Programming Languages(PPL 2015) 17 2015
名目書き換えシステムの合流性について Reviewed
The 16th JSSST Workshop on Programming and Programming Languages(PPL 2014) 16 2014
帰納的定理自動証明のための項書き換えシステム自動変換 Reviewed
The 16th JSSST Workshop on Programming and Programming Languages(PPL 2014) 16 2014
閉包操作に基づく右基底項書き換えシステムの到達可能性判定 Reviewed
The 16th JSSST Workshop on Programming and Programming Languages(PPL 2014) 16 2014
永続性と減少ダイアグラム法に基づく合流性自動証明 Reviewed
The 16th JSSST Workshop on Programming and Programming Languages(PPL 2014) 16 2014
書き換え帰納法に基づく帰納的定理の決定可能性 Reviewed
The 15th JSSST Workshop on Programming and Programming Languages(PPL 2013) 15 2013
ボトムアップ書き換えに基づく最内書き換え到達可能性判定 Reviewed
The 15th JSSST Workshop on Programming and Programming Languages(PPL 2013) 15 2013
片側減少ダイアグラム法による項書き換えシステムの可換性証明法 Reviewed
The 14th JSSST Workshop on Programming and Programming Languages(PPL 2012) 14 2012
Transformations by templates for simply-typed term rewriting
Takahito Aoto, Yuki Chiba
6th International Workshop on Higher-Order Rewriting (HOR 2012) 2012
永続性にもとづく項書き換えシステムの合流性証明 Reviewed
The 14th JSSST Workshop on Programming and Programming Languages(PPL 2012) 14 2012
基底項書き換え系の多項式時間合流性判定法の改良 Reviewed
The 13th JSSST Workshop on Programming and Programming Languages(PPL 2011) 13 2011
多項式サイズ正規形を保証する項書き換えシステムの経路順序 Reviewed
The 13th JSSST Workshop on Programming and Programming Languages(PPL 2011) 13 2011
無限項書き換えシステムにおける強頭部正規化可能性の反証手続き Reviewed
The 12th JSSST Workshop on Programming and Programming Languages(PPL 2010) 12 2010
拡大手法に基づく項書き換え系の合流性自動証明 Reviewed
The 12th JSSST Workshop on Programming and Programming Languages(PPL 2010) 12 2010
項書き換えシステムの合流性判定, Reviewed
The 10th JSSST Workshop on Programming and Programming Languages(PPL 2008) 10 2008
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
反証機能付き書き換え帰納法のための補題自動生成法 Reviewed
The 10th JSSST Workshop on Programming and Programming Languages(PPL 2008) 10 2008
Automating Confluence Check of Term Rewriting Systems. Reviewed
Junichi Yoshida, Takahito Aoto, Yoshihito Toyama
Information Technology Letters 6 31 - 34 2007
書き換え帰納法における向き付け不能な等式の証明 Reviewed
The 8th JSSST Workshop on Programming and Programming Languages(PPL 2006) 8 2006
Introducing Sequence Variables in Program Transformation Based on Templates. Reviewed
Yuki Chiba, Takahito Aoto, Yoshihito Toyama
Information Technology Letters 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
Proving Inductive Theorems of Higher-Order Functional Programs. Reviewed
Takahito Aoto, Toshiyuki Yamada, Yoshihito Toyama
Information Technology Letters 2 21 - 22 2003
ソフトウェア科学会 研究論文賞
2017 ソフトウェア科学会 項書き換えシステムの変換を利用した帰納的定理自動証明
佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
第12回プログラミングおよびプログラミング言語ワークショップ論文賞
2012.3 第12回プログラミングおよびプログラミング言語ワークショッププログラム委員会
鈴木翼, 青戸等人, 外山芳人
第２回情報科学技術フォーラム論文賞
2003.9 情報処理学会
青戸等人, 山田俊行, 外山芳人
項書き換えシステムの解の一意性を保証する性質に関する研究
Grant number：21K11750
2021.4 - 2024.3
System name：科学研究費助成事業
Research category：基盤研究(C)
Awarding organization：日本学術振興会
青戸 等人
Grant amount：\4160000 （ Direct Cost: \3200000 、 Indirect Cost：\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性についても永続性を利用した検証手法が考案するのに役立つと考えられる．また，指向式条件付き項書き換えシステムのレベル可換性を保証する条件や局所十分完全性を保証する条件についても新しい条件を与えた．
Inductive thoeorems and ground confluence for conditional term rewriting systems
Grant number：18K11158
2018.4 - 2022.3
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
Aoto Takahito
Grant amount：\4420000 （ Direct Cost: \3400000 、 Indirect Cost：\1020000 ）
Term rewriting is a model of computation based on equational logic. The notion of inductive theorems of term rewriting systems expresses validity of equations from the programming perspective, and conditional term rewriting systems are a rewriting framework that suits to model functional programs, based on horn-clause logic. In this project, we give a rewriting induction framework to prove horn-clause inductive theorems over conditional term rewriting systems. We also give a method to prove ground confluence of oriented conditional term rewriting systems, as well as a critical pairs criterion for level-commutativity of oriented conditional term rewriting systems, etc.
Program Verification Methods based on Context-Moving Transformation and Higher-Order Rewriting Theory
Grant number：16K00091
2016.4 - 2019.3
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
KIKUCHI Kentaro
Grant amount：\3510000 （ Direct Cost: \2700000 、 Indirect Cost：\810000 ）
We conducted research to develop new methods for program verification based on rewriting techniques. The main results of this research are summarised as follows:
(1) Concerning rewriting systems with variable binding, we obtained several new conditions on confluence of nominal rewriting systems and other related systems. Also, we have taken part in the development of automated confluence and termination provers for versions of higher-order rewriting systems, and achieved excellent results in international competitions.
(2) Through observations on inductionless induction methods in rewriting systems without the sufficient completeness property, we developed a new verification method that is applicable to programs including those expressions which induce non-terminating computation such as infinite lists.
Study on Ground Confluence of Rewrite Systems
Grant number：15K00003
2015.4 - 2018.3
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
Aoto Takahito
Grant amount：\4550000 （ Direct Cost: \3500000 、 Indirect Cost：\1050000 ）
Ground confluence of term rewriting systems is a property fundamental to establish software verification techniques based on rewrite systems. In this study, we have focused on rewriting induction which a method for inductive theorem proving, and have shown that bounded convertibility guarantees the ground confluence. We have designed a rewriting induction method for establishing bounded convertibility and have shown its correctness theoretically. We have also given a method to deal with the case in which suitable rules are not presented in the input system, a method to deal with non-orientable constructor rules, and a method to deal with disproving ground confluence. Based on the proposed methods we have implemented in ground confluence prover AGCP.
Research on automated program verification based on confluence
Grant number：25330004
2013.4 - 2016.3
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
toyama yoshihito, AOTO TAKAHITO
Grant amount：\4550000 （ Direct Cost: \3500000 、 Indirect Cost：\1050000 ）
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although several automated confluence provers of term rewriting systems have been developed recently, little work is reported on applications of them. This research aims to develop automated program verification methods based on automated confluence provers for term rewriting systems. Concrete results include confluence proving based on persistency and type information, automated inductive theorem proving based on program transformations, sufficient criteria for confluent nominal rewriting systems, a sufficient condition for termination of the tree automata completion, automated ground confluence proving, abstract reduction systems on ordered monoid.
Lemma Generation in Inductive Theorem Proving
Grant number：23500002
2011 - 2013
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
AOTO takahito, TOYAMA Yoshihito
Grant amount：\5070000 （ Direct Cost: \3900000 、 Indirect Cost：\1170000 ）
Our focus in this project is inductive theorem proving based on term rewriting systems. We are interested in identifying lemmas that leads the whole inductive theorem proving procedure to success. Our first attempt to this problem lies in how to extract information from divergence of proving procedure. For this, we investigated theories of unification and rewriting of regular terms and semi-unification that suits for expressing and detecting looping structures. We extended decision procedure for inductive theorems based on rewriting induction, and also we give a novel decision procedure of inductive theorems based on a new approach employing decision procedures for validity in initial algebras. We also studied how one can extract suitable properties from tail-recursive function definition for translating them to equivalent simple recursive one.
Research on automated confluence proving for term rewriting systems
Grant number：22500002
2010 - 2012
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
TOYAMA Yoshihito, AOTO Takahito
Grant amount：\3640000 （ Direct Cost: \2800000 、 Indirect Cost：\840000 ）
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although many automated termination provers of term rewriting systems have been proposed recently, little work is reported on automated confluence provers. This research aims to develop an automated confluence prover ACP for term rewriting systems based on several methods. Concrete results include a reduction-preserving completion method for proving confluence, one side decreasing diagram method for proving commutativity, a path ordering for guaranteeing polynomial size normal forms, a confluence proof method based on persistency. In the first confluence competition for term rewriting systems (IWC 2012), ACP developed by our group has won first place among the three participants.
Combining Rippling and Rewriting Induction for Inductive Theorm Proving
Grant number：20500002
2008 - 2010
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
AOTO Takahito, TOYAMA Yoshihito
Grant amount：\3640000 （ Direct Cost: \2800000 、 Indirect Cost：\840000 ）
Our focus in this project is inductive theorem proving based on term rewriting systems. We are, in particular, interested in rewriting induction methods. We extended rewriting induction to enhance provability of non-orientable conjectures, and we implemented an inductive theorem prover based on our extension. Lemma discovery is an important aspect of inductive theorem proving and we generalized a sound generalization technique and gave sound divergence critic, which are useful when the rewriting induction is equipped with the disproving mechanism. We propose rewriting induction framework to incorporate different lemma generation methods. We also investigate automated confluence proving, as it is a necessary property to extend rewriting induction with the disproving mechanism. We gave new techniques to prove confluence and implemented a confluence prover.
Research on program transformation systems based on automated theorem proving
Grant number：19500003
2007 - 2009
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
TOYAMA Yoshihito, AOTO Takahito
Grant amount：\3770000 （ Direct Cost: \2900000 、 Indirect Cost：\870000 ）
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. This research aims to develop basic theories and prototypes for automated program transformation systems based on term rewriting theory. Concrete results include an automated construction method of program transformation templates, a new termination proof of higher-order programs, an automated lemma generation method for rewriting induction, an automated confluence prover of term rewriting systems.
高階関数を用いたプログラム検証および変換技術の高度化に関する研究
Grant number：17700002
2005 - 2007
System name：科学研究費助成事業
Research category：若手研究(B)
Awarding organization：日本学術振興会
青戸 等人
Grant amount：\1700000 （ Direct Cost: \1700000 ）
単純型付き項書き換えシステムの停止性検証手法の高度化を以下の点について試みた。(1)依存対手法における引数フィルタリングおよび使用可能規則を高階の場合への拡張を行った。(2)実験システムについての検討を進めた。特に、効率的な実装を実現するためのSAT検証器を用いた実装法についての検討を行い、その基本となる経路順序の符号化法について改良を行った。また停止性にもとづく帰納的定理の自動証明法である書き換え帰納法についての検討を進めた。特に反証付き書き換え帰納法に適した補題自動導入法について検討を行った。発散鑑定法を改良し、健全性を持つ発散鑑定法を提案した。実験システムを実装するとともに証明システムのベンチマークとなる例題集を抽出し、他の書き換え帰納法に基づく定理証明器との比較実験を行った。また、反証付き書き換え帰納法を利用するために必要な合流性を保障する方法について検討を進めた。停止性の検証器は多数提案されているのに対して、合流性の検証器の提案はあまりなされていないため、合流性の自動検証法について実験システムを構築し検討を行った。合流性の十分条件を満たさない項書き換えシステムについて分解手法を用いる判定法を利用することの検討を行い、分解手法を利用した合流性検証器の提案を行った。変換パターンに基づくプログラム変換のための変換パターンの抽出法について検討をすすめた。2階の一般化アルゴリズムを提案し、それに基づいて具体的なプログラム変換から変換パターンを抽出する実験を行った。変換に利用可能なパターンの抽出を容易にするためのヒューリスティクスについて検討を行い、いくつかの変換パターンの抽出に成功した。
完備化に基づくプログラム自動変換の研究
Grant number：16016202
2005
System name：科学研究費助成事業
Research category：特定領域研究
Awarding organization：日本学術振興会
外山 芳人, 青戸 等人, 菊池 健太郎
Grant amount：\4500000 （ Direct Cost: \4500000 ）
プログラム変換の手法である融合変換と、定理自動証明の手法である完備化を組み合わせた新しいプログラム変換手法を提案することを目的として、プログラム変換の実験と解析を行った。とくに、帰納的定理の強力な自動証明手法である書き換え帰納法と組み合わせることによって、プログラム変換に必要な性質を自動証明しながら、その結果を利用してプログラム変換を進めていくので、従来よりも強力な変換が可能となる。また、変換に必要な性質を自動的に発見することを可能とする補題発見機構を組み入れることにより、高度なプログラム自動変換を実現することができることを実証することができた。
さらに、パターンをもちいたプログラム変換システムRAPTを開発した。これまでの研究から、プログラムの効率化にはいくつかの定石があることが明らかになっている。そこで、これらの定石を高階の変換パターンで表現し、パターンマッチングによるプログラム変換で効率を改良する方法を提案した。変換の正当性を検証するためには、プログラムのさまざまな帰納的性質を証明する必要がある。そこで、プログラムを書き換えシステムでモデル化し、定理自動証明の手法である潜在帰納法を適用することにより、プログラム変換とその正当性の検証を完全に自動化することに成功した。RAPTは入力プログラムを自動変換して出力プログラムを得るまでの手続きを6段階に分けて実現している。実装は関数型言語SMLをもちいて行い、ソースコードのサイズは約5000行である。
また、プログラムの変換や検証に不可欠な基礎技術である高階プログラムの帰納的性質や停止条件に関する理論的な解析を進めるとともに、プログラムの実行メカニズムの設計に不可欠なリダクションの戦略に関する基礎理論の確立を行った。
完備化に基づくプログラム自動変換の研究
Grant number：15017203
2003
System name：科学研究費助成事業
Research category：特定領域研究
Awarding organization：日本学術振興会
外山 芳人, 青戸 等人
Grant amount：\2100000 （ Direct Cost: \2100000 ）
完備化に基づくプログラム融合変換のアイデアを,高階プログラムに適用するためには,高階書き換えシステムの完備化を実現する必要がある。しかし,高階書き換えシステムの完備化手続きの多くは机上の提案にとどまっており,実装にはいたっていない。これは,完備化手続きを実装するために不可欠な高階書き換えシステムの停止性が,簡単に判定できなかったからである。
本研究では,項の幅の上界を設定することで,固定次数の関数記号に対する単純化順序の定義が,可変次数の関数記号に対してもそのまま有効に働くことに注目し,S式書き換えシステムの停止性が辞書式経路順序で簡単に判定できることを示した。実際に利用される高階書き換えシステムの多くは,S式書き換えシステムで表現できるため,ここで提案された停止性判定法をもちいて完備化可能である。我々は,S式書き換えシステムの完備化手続きを計算機上に実装し,高階書き換えシステムの完備化と融合変換が容易に実現できることを実験によって明らかにした。
さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,高階関数を含む帰納的定理の自動証明法を検討し,高階書き換えシステムにおける潜在帰納法の枠組みを提案するとともに,潜在帰納法の適用に不可欠な十分完全性の判定が決定可能であることを明らかにした。
また,書き換え代入に基づく2階のパターンマッチングを提案し,パターマッチングをもちいたプログラム変換手続きを改良するとともに,書き換え帰納法に基づく高階プログラムの融合変換の実験を行った。
Program verification method based on reduction approximations
Grant number：14580357
2002 - 2005
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
TOYAMA Yoshihito, AOTO Takahito, KIKUCHI Kentarou
Grant amount：\2800000 （ Direct Cost: \2800000 ）
To propose program verification techniques based on reduction approximations, we have studied. rewriting theories among normalization reduction strategies, program transformation by template, termination of higher-order rewriting systems, automated proving for higher-order inductive theorems, decidability of reachability problem. Thorough theoretical analysis and experiments, we have obtained the following results.
(1)We proposed the notion of normalizing strategy based on balanced weak confluence. It was shown that external reduction is a normalizing strategy for left-linear term rewriting systems if every critical pair is root balanced joinable. This results expands normalizing strategy of needed reduction. We also presented that external reduction is a computable reduction strategy if regular preserving approximation if it exits.
(2)We developed a framework of program transformation by template based on rewriting systems. The correctness of our program transformation method is proven without explicit use of induction on data structures. Thus our program transformation system can easily incorporate with automated theorem provers.
(3)We introduce the notion of growing approximation, which is a generalization of strong sequential approximation, NV-sequential approximation and right-linear growing approximation. We have shown that the growing approximation extends the class of term rewriting systems having a decidable normalizing strategy. Moreover, the decidability of confluence and termination for growing systems is presented.
宣言型プログラミング言語のためのAC記号のあるナローイングの計算理論
Grant number：14780187
2002 - 2004
System name：科学研究費助成事業
Research category：若手研究(B)
Awarding organization：日本学術振興会
青戸 等人
Grant amount：\1100000 （ Direct Cost: \1100000 ）
前年度に得られた高階項書き換え系における帰納的定理証明について解析を進めた.第1階の場合には自明に成立するが,高階では一般に成立しない帰納的定理の性質が単調性である.単調性を満たさないと高階帰納的定理の利用に様々な制約が課せられる.そこで,我々は,高階帰納的定理が単調性を持つための条件について考察した.まず,第1階項書き換え系における十分完全性の概念を拡張し,高階十分完全性の概念を与えた.そして,この概念を用いて,等式が単調高階帰納的定理となるための十分条件を明らかにした.次に,高階十分完全性の自動証明について考察を行なった.高階十分完全性の自動証明を行うため,初等性および高階図式という制約を導入し,高階十分完全性が決定可能となる単純型付き項書換え系のクラスを与えた.初等的な高階図式は多くの自然な高階関数プログラムを含む.以上の結果は,項書き換え分野の代表的な国際会議の1つであるRTA(書き換え技法と応用)'04に採録され,国際的な報告を行なった.
前年度に得られた,単純型付き項書き換え系の停止性証明技法の実装について検討を行なった.その実装の第一段階として,より単純な体系である単純型付き適応的項書き換え系の停止性証明技法について考察を行なった.その過程で,適応的項書き換え系についてのみ適用可能な,非常に簡単で,しかも比較的強力な停止性証明技法を考案した.この成果は高階項書き換え系の国際ワークショップHOR'04に採録され,国際的な報告を行なった.
Applications of Mathematical Logic in Theoretical Computer Science
Grant number：08680356
1996 - 1997
System name：Grants-in-Aid for Scientific Research
Research category：Grant-in-Aid for Scientific Research (C)
Awarding organization：Japan Society for the Promotion of Science
ONO Hiroakira, AOTO Takahito, KASHIMA Ryo, ISHIHARA Hajime, TOYAMA Yoshihito
Grant amount：\2400000 （ Direct Cost: \2400000 ）
Main aim of this project is to study various logical problems appearing in computer science from both theoretical and practical point of view. In particular, we planned to bring the following subjects into focus, at the beginning.
1. linear logic and substructural logics, in general, as logic of action and logic of resources,
2. reasoning about knowledge, based on epistemic logic and cummulative reasoning,
3. descriptions of specifications of software based on temporal logics and their verifications,
4. reduction systems, in particular, term rewriting systems, and their applications to functional programming languages.
1. One is now developing a general theory of substructural logics without contraction rule, by using algebraic methods. The study shows that within the framework of logics without contraction rule, we can discuss various kinds of logics, including BCK logics, intuitionistic logic, Lukasiewicz's many-valued logics and even some of fuzzy logics in a uniform way. Ishihara and Kashima discussed various implicational logics and their connections with typed lambda calculi.
2. Some studies has been done by One in belief revision and its relation to reasoning of other types, like inductive reasoning and cummulative reasoning.
3. A very important theoretical study has been done by F.Wolter, who was a member of our project in 1996. Among others, he obtained strong results on the decision problems on temporal logics. This topics is related also to modal logic. Aoto and Ono have developed the study of the intuitionistic modal logics in collaboration with F.Wolter, M.Zakharyaschev and G.Bezhanishvili, who stayd at JAIST at least a half of the term of the present project.
4. Toyama and Aoto obtained interesting results on term rewriting systems, in particular on the termination, the confluence and the modularity of these systems, in collaboration with M.Sakai who was a member of our project in 1996.
リメディアル演習
総合工学概論
プログラミングAIII
工学リテラシー入門
知能情報システム概論
計算論理学
形式言語とオートマトン
数理論理学
情報数理演習III
情報工学演習
情報工学基礎実習II
情報工学基礎実習I
コンピュータへの招待
リメディアル演習
総合工学概論
計算モデル特論
卒業研究
研究室体験実習
自然科学総論Ⅲ
プログラミングAIII
論文輪講
卒業研修
工学リテラシー入門(情報電子分野)
知能情報システム概論
計算論理学
形式言語とオートマトン
情報数理演習III
情報工学基礎実習II
情報工学基礎実習I
コンピュータへの招待
技術英語入門
数理論理学
