Reports and Others

• 笠鳥謙太, 青戸等人,
  方向付け不能なホーン節に対する書き換え帰納法,
  第146回プログラミング研究発表会, 東京工業大学およびオンラインのハイブリッド開催, 2023-3-(3), 2023年10月31日〜11月1日.

• 櫻井爽一, 青戸等人,
  項書き換えシステムにおける生成性と局所十分完全性について,
  第146回プログラミング研究発表会, 東京工業大学およびオンラインのハイブリッド開催, 2023-3-(2), 2023年10月31日〜11月1日.

• 井出政宏, 青戸等人,
  論理制約付き項書き換えシステムにおける末尾再帰変換の正当性証明と実装,
  日本ソフトウェア科学会第40回大会, ポスター・デモ, 3-P-S, 2023.

• 東幸輝, 青戸等人,
  条件付き項書き換えシステムの危険対条件に基づく合流性検証,
  日本ソフトウェア科学会第40回大会, ポスター・デモ, 4-P-S, 2023.

• 長橋謙, 青戸等人,
  合流性に基づく交差式条件付き項書き換えシステムのアンラベリング変換の健全性条件,
  第142回プログラミング研究発表会, 広島(ハイブリッド開催), 2022-4-(7), 2023年1月12日〜13日.

• 渡邉廉, 青戸等人,
  永続性を利用した項書き換えシステムの一意正規形性の検証,
  第141回プログラミング研究発表会, 東京(ハイブリッド開催), 2022-3-(4), 2022年10月27日〜28日.

• 冨田也斗, 青戸等人,
  関数型プログラムから論理制約付き条件付き項書き換えシステムへの変換,
  第141回プログラミング研究発表会, 東京(ハイブリッド開催), 2022-3-(3), 2022年10月27日〜28日.

• 望月美希, 青戸等人,
  正則項書き換えにおける書き換えステップの決定可能性について,
  日本ソフトウェア科学会第39回大会, 43-S, 2022.

• 趙順, 青戸等人,
  フラット右線形項書き換えシステムの簡約に関する一意正規形性の決定不能性の証明について,
  日本ソフトウェア科学会第39回大会, 42-S, 2022.

• 南山駿人, 青戸等人,
  書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合,
  第136回プログラミング研究発表会, オンライン開催, 2021-3-(9), 2021年11月1日〜11月2日.

• 大野峻, 青戸等人,
  交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について,
  第136回プログラミング研究発表会, オンライン開催, 2021-3-(4), 2021年11月1日〜11月2日.

• 芳賀雅樹, 青戸等人,
  置換に関する不動点制約を用いた名目書き換え,
  第136回プログラミング研究発表会, オンライン開催, 2021-3-(3), 2021年11月1日〜11月2日.

• 佐藤悠稀, 青戸等人,
  フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性,
  第131回プログラミング研究発表会, オンライン開催, 2020-3-(8), 2020年10月29日〜30日.

• 笹川葵生, 青戸等人,
  外部変数のある可換式条件付き項書き換えシステムの合流性条件,
  第131回プログラミング研究発表会, オンライン開催, 2020-3-(7), 2020年10月29日〜30日.

• 宮前海里, 青戸等人,
  圏論にもとづく正則項上の単一化の形式化,
  第131回プログラミング研究発表会, オンライン開催, 2020-3-(4), 2020年10月29日〜30日.

• 芳賀亮太, 青戸等人,
  危険対条件に基づく条件付き項書き換えシステムの階層可換性,
  日本ソフトウェア科学会第38回大会, 41-L, 2021.
  [pdf]

• 東和田直輝, 青戸等人,
  条件付き項書き換えシステムの十分完全性の自動証明,
  第124回プログラミング研究発表会, 名古屋大学, 2019-1-(4), 2019.

• 白石智輝, 青戸等人,
  項書き換えシステムにおける局所十分完全性の証明法の提案,
  第124回プログラミング研究発表会, 名古屋大学, 2019-1-(5), 2019.

• 加賀谷有輝, 青戸等人,
  条件付き項書き換えシステムの階層合流性証明法,
  第124回プログラミング研究発表会, 名古屋大学, 2019-1-(6), 2019.

• 石塚守, 青戸等人,
  Jaffarのアルゴリズムに基づく正則項の単一化,
  日本ソフトウェア科学会第35回大会, PPL3-4-S, 2018.
  [pdf, 7 pages]

• 山口諒, 青戸等人,
  決定手続きを用いた項書き換えシステムの帰納的定理自動証明,
  日本ソフトウェア科学会第35回大会, PPL2-3-S, 2018.
  [pdf, 7 pages]

• Takahito Aoto and Yoshihito Toyama,
  Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems,
  CoRR abs/1807.00940, 2018.

• 加藤裕人, 青戸等人
  書き換え帰納法を利用した帰納的定理証明の補題生成法
  日本ソフトウェア科学会第34回大会, PPL4-1, 2017.
  [pdf, 8 pages]

• 萩原崇央, 青戸等人
  極大完備化に基づく等式定理の自動証明
  日本ソフトウェア科学会第34回大会, PPL2-1, 2017.
  [pdf, 5 pages]

• 菊池健太郎, 青戸等人, 外山芳人
  文脈移動法によるプログラム変換の正当性について
  日本ソフトウェア科学会第32回大会, PPL4-4, 2015.
  [pdf, 4 pages]

• Koichi Sato, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama
  Context-moving transformation for term rewriting systems
  2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), Warsaw, Poland, July 2015
  [abstract]

• Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
  Correctness of Context-Moving Transformations for Term Rewriting Systems
  25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), Siena, Italy, July 2015.
  [abstract]

• Takahito Aoto and Munehiro Iwami
  Uniform semi-unification
  「計算機科学における論理・代数・言語」研究集会報告集, 数理解析研究所講究録, Vol.1915, pp.161-165, 京都大学数理解析研究所, 2014.
  

• 佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
  自動検証のためのプログラム変換
  日本ソフトウェア科学会第30回大会, PPL5-5, 2013.
  [pdf, 9 pages]

• 四方駿作, 青戸等人, 外山芳人
  閉包操作に基づく項書き換えシステムの到達可能性判定
  日本ソフトウェア科学会第30回大会, PPL5-4, 2013.
  [pdf, 5 pages]

• 内田和真, 青戸等人, 外山芳人
  永続性と減少ダイアグラム法に基づく合流性証明法
  日本ソフトウェア科学会第30回大会, PPL4-1, 2013.
  [pdf, 7 pages]

• 椛澤涼, 青戸等人, 外山芳人
  木オートマトンに基づく項書き換えシステムの逆計算
  日本ソフトウェア科学会第29回大会, 3B-4, 2012.
  [pdf, 4 pages]

• 高橋翔大, 青戸等人, 外山芳人
  ボトムアップ書き換えに基づく到達可能性の判定法
  日本ソフトウェア科学会第29回大会, 3B-3, 2012.
  [pdf, 6 pages]

• 中嶋辰成, 青戸等人, 外山芳人
  書き換え帰納法に基づく帰納的定理の決定手続き
  日本ソフトウェア科学会第29回大会, 3B-2, 2012.
  [pdf, 4 pages]

• 岩見宗弘, 青戸等人
  無限項書き換えシステムにおける性質に関する考察
  「代数と言語のアルゴリズムと計算理論」研究集会報告集, 数理解析研究所講究録, Vol.1769, pp.153-157, 京都大学数理解析研究所, 2011.
  

• 的場正樹, 青戸等人, 外山芳人
  減少ダイアグラム法による項書き換えシステムの可換性証明法
  日本ソフトウェア科学会第28回大会, 1A-3, 2011.
  [pdf, 5 pages]

• 鈴木翼, 青戸等人, 外山芳人
  永続性にもとづく項書き換えシステムの合流性証明
  日本ソフトウェア科学会第28回大会, 1A-2, 2011.
  [pdf, 5 pages]

• Jeroen Ketema, Stefan Blom, Takahito Aoto, and Jakob Grue Simonsen
  Rewriting transfinite terms
  Liber Amicorum for Roel de Vrijer, pp.129-144. 2009.
  [pdf, 16 pages]

• 青戸等人
  停止性検証器を利用した書き換え帰納法手続き
  日本ソフトウェア科学会第24回大会, 3C-2, 2007.
  [pdf, 4 pages]

• 五十嵐圭一，青戸等人, 外山芳人
  項書き換えシステム停止性検証におけるSATソルバ利用のための新しい符号化法
  日本ソフトウェア科学会第24回大会, 3C-1, 2007.
  [pdf, 6 pages]

• 千葉勇輝, 青戸等人, 外山芳人
  項書き換えシステム自動変換のための2階一般化アルゴリズムについて
  日本ソフトウェア科学会第24回大会, 2C-2, 2007.
  [pdf, 5 pages]

• 千葉勇輝, 青戸等人, 外山芳人
  プログラム変換パターンの自動生成
  第64回プログラミング研究会(PRO-2007-1), 2007.

• 青戸等人
  抽象原理に基づく書き換え帰納法の健全性
  第64回プログラミング研究会(PRO-2007-1), 2007.

• 千葉勇輝, 青戸等人, 外山芳人
  Program transformation by templates: A rewriting framework
  第59回プログラミング研究会(PRO-2006-1), 2006.

• 千葉勇輝, 青戸等人, 外山芳人
  パターンに基づくプログラム変換システム
  日本ソフトウェア科学会第22回大会, 3A-1, 2005.
  [pdf, 5 pages]

• 落合秀幸, 青戸等人, 外山芳人
  修正AC単調意味論経路順序によるAC停止性
  信学技報 COMP2004-76, Vol.104, No.743, pp.23-31, 電子情報通信学会, 2005.

• 坂本邦彦, 青戸等人, 外山芳人
  書き換え帰納法に基づくプログラム融合変換
  日本ソフトウェア科学会第21回大会, 2B-3, 2004.
  [ps, 4 pages]

• Yuki Chiba, Takahito Aoto and Yoshihito Toyama
  Term pattern matching with tree homomorphism
  第49回プログラミング研究会(PRO-2004-1), 2004.

• 秋谷賢司, 青戸等人, 外山芳人
  優先順序付き書き換えの計算モデル
  信学技報 COMP2003-85, Vol.103, No.722, pp.31-38, 電子情報通信学会, 2004.

• Takahito Aoto and Takashi Nagaya
  Decidable/undecidable properties of conditional term rewriting systems
  京都大学数理解析研究所共同研究集会「言語，代数系および計算機システム」, 数理解析研究所講究録, Vol.1106, pp.1-12, 京都大学数理解析研究所, 1999.

• Takahito Aoto and Takashi Nagaya
  Decidable/undecidable properties of conditional term rewriting systems
  Research Report IS-RR-98-0030F, School of Information Science, JAIST, December 1998.
  [ps, 19 pages]

• Takahito Aoto
  A proof of the conjecture of Zantema on a persistent property of term rewriting systems
  Research Report IS-RR-98-0008F, School of Information Science, JAIST, February 1998.
  [ps, 16 pages]

• Takahito Aoto and Hiroyuki Shirasu
  On the finite model property of intuitionistic modal logics over MIPC
  Research Report IS-RR-98-0004F, School of Information Science, JAIST, January 1998.
  [ps, 16 pages]

• Takahto Aoto and Yoshihito Toyama
  Tree lifting orderings for termination transformations of term rewriting systems
  LAシンポジウム, 那覇, 情報基礎理論ワークショップ, pp.109-114, 1997.

• Takahito Aoto and Yoshihito Toyama
  Tree lifting orderings for termination transformations of term rewriting systems
  Research Report IS-RR-97-0033F, School of Information Science, JAIST, August 1997.
  [ps, 19 pages]

• Takahito Aoto and Yoshihito Toyama
  Top-down labelling and modularity of term rewriting systems
  情報基礎理論ワークショップ, pp.166-171, 1996.

• Takahito Aoto and Yoshihito Toyama
  Extending persistency of confluence with ordered sorts
  信学技報 COMP96-31, Vol.96, No.250, pp.29-38, 電子情報通信学会, 1996.

• Takahito Aoto and Yoshihito Toyama
  Extending persistency of confluence with ordered sorts
  Research Report IS-RR-96-0025F, School of Information Science, JAIST, August 1996.
  [ps, 21 pages]
  

• Takahito Aoto and Yoshihito Toyama
  Top-down labelling and modularity of term rewriting systems
  Research Report IS-RR-96-0023F, School of Information Science, JAIST, August 1996.
  [ps, 21 pages]
  

• Takahito Aoto and Yoshihito Toyama
  Persistency of confluence
  Research Report IS-RR-96-0009F, School of Information Science, JAIST, March 1996.
  [ps, 18 pages]
  

• Takahito Aoto
  Unique normal proof property for implicational minimal formulas in the intuitionistic logic
  Research Report IS-RR-95-0015F, School of Information Science, JAIST, August 1995.
  [ps, 33 pages]

• Takahito Aoto and Hiroakira Ono
  Uniqueness of normal proofs in { \to, \land }-fragment of NJ
  Research Report IS-RR-94-0024F, School of Information Science, JAIST, August 1994.
  [ps, 20 pages]