青戸研究室

ゼミの記録

2023年度

輪講

(2023/4/25開始)
George E. Andrews, Number Theory, 1971
参加者：石田，滝沢，林，三角，能澤，笠鳥，井伊，青戸
(2023/4/25開始)
Software Foundations, Volume 1: Logical Foundations, https://softwarefoundations.cis.upenn.edu/lf-current/index.html
参加者：加藤，山本，嶋貫，高畑，井出，櫻井，東，青戸

論文(解説)紹介

(紹介者：石田,2023/12/21)
栗田泰智, 青戸等人, 条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明, コンピュータソフトウェア, Vol.36, No.2, pp.61-75, 2019.
(紹介者：林,2023/12/14)
C. Kop, N. Nishida, Term Rewriting with Logical Constraints, In Proc. of 9th FroCoS, LNAI, Vol.8152, pp.343-358, 2013.
(紹介者：山本,2023/12/7)
C. Sternagel, T. Sternagel, Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems, In Proc. of 26th CADE, LNAI, Vol.10395, pp.413-43, 2017.
(紹介者：三角,2023/11/30)
R. Gutierrez, S. Lucas, M. Vitores, Confluence of Condititonal Rewriting in Logical Form, In Proc. of 41st FSTTCs, LIPIcs, Vol.44, pp.44:1-44:18, 2021.
(紹介者：滝沢,2023/11/16)
J. Nagele, B. Felgenhauer and A. Middeldorp, Improving Autumatic Confluence Analysis of Rewrite Systems by Redundant Rules, In Proc. of 26th RTA, LIPIcs, Vol.36, pp.257-268, 2015.
(紹介者：加藤,2023/11/9)
T. Aoto, Y. Toyama, Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems, In Proc. of 12th FroCoS, LNAI, Vol.12, pp.330-347, 2019.
(紹介者：伊井,2023/8/5)
N. Hirokawa, J. Nagele, V. van Oostrom, and M. Oyamaguchi, Confluence by Critical Pair Analysis Revisited, In Proceedings of International Conference on Automated Deduction (CADE 2019), pp.319-336, LNCS 11716, 2019, Springer.
(紹介者：嶋貫,2023/8/1)
Chapter 3 of Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.
(紹介者：高畑,2023/6/8,15)
N. Dershowitz and U.S. Reddy, Deductive and Inductive Synthesis of Equational Programs, Journal of Symbolic Computation, Vol.15, pp.467-494, 1993.

2022年度

輪講

(2022/5/13開始，2023/2/9終了，3.4節まで)
Samuel Mimram, Program = Proof, 参加者：嶋貫，高畑，中村，長岡，能澤，櫻井，東，趙，望月，青戸
(2022/5/13開始，2023/2/8終了，2章まで)
Arkadii Slinko, Algebra for Applications, Springer, 2020
参加者：伊井，小口，本間，井出，笠鳥，趙，冨田，長橋，渡邊，青戸

論文(解説)紹介

(紹介者：本間，2023/2/9)
岩見宗弘,正則項の木変換器による書き換え,JSSST大会, 2022.
(紹介者：長岡，2023/2/2)
T. Aoto, Disproving confluence of term rewriting systems by interpretation and ordering, In Proc. of 9th FroCoS, LNAI, Vol.8152, pp.311-326, 2013.
(紹介者：嶋貫，2023/1/26)
James Brotherston, Alex, Simpson, Sequent calculi for induction and infinite descent, Journal of Logic and Computation, Vol.21, No.6, pp.1177–1216, 2011.
(紹介者：高畑,2023/1/19)
C. Kop, N. Nishida, Term Rewriting with Logical Constraints, In Proc. of 9th FroCoS, LNAI, Vol.8152, pp.343–358, 2013.
(紹介者：中村,2022/12/12)
S. Winkler, A. Middeldorp, Completion for logically constrained rewriting, In Proc. of 3rd FSCD, LIPIcs, Vol.108, pp.30:1-30:18, 2018.
(紹介者：井伊,2022/12/8)
T． Aoto and J． Ketema, Rational term rewriting revisited: decidability and confluence, In Proc． of 6th ICGT,LNCS, Vol.7562, pp.172-186, 2012, Springer-Verlag.
(紹介者：櫻井,2022/7/28)
J. Endrullis, D. Hendriks, Lazy Productivity via Termination, Theoretical Computer Scince, Vol.412, pp.3203–3225, 2011.
(紹介者：東,2022/7/21)
R． Gutierrez, S. Lucas, Automatically Proving and Disproving Feasibility Conditions, In Proc. of 10th IJCAR, LNAI, Vol.12167, pp.416–435, 2020.
(紹介者：笠鳥,2022/7/14)
T. Aoto, Y. Toyama, Ground Confluence Prover Based on Rewriting Induction, In Proc. of 1st FSCD, LIPIcs, Vol.33, pp.33:1-33:12, 2016.
(紹介者：井出,2022/7/7)
C. Kop, N. Nishida, Term Rewriting with Logical Constraints, In Proc. of 9th FroCoS, LNAI, Vol.8152, pp.343–358, 2013.

2021年度

輪講

(2021/4/28開始，2022/2/7終了，2.6節まで)
Harold Simmons, An Introduction to Category Theory, Cambridge University Press, 2011.
参加者：笠鳥，齋藤，渋谷，東，趙，冨田，望月，渡邊，芳賀(り)，南山，青戸
(2021/4/28開始，2022/2/9終了，6章まで)
Hiroakira Ono, Proof Theory and Algebra in Logic, Springer, 2010
参加者：井出，櫻井，長橋，大野，芳賀(ま)，青戸
(2017/11/29開始，2021/6/11終了，読了)
. Steve Awodey, Category Theory, Oxford University Press, 2010.
参加者：高橋，青戸

論文(解説)紹介

(紹介者：長橋,2022/2/15)
K. Gmeiner, B. Gramlich and F. Schernhammer, On (Un)Soundness of Unravelings, In Proc. of 21st RTA, pp.119--134, LIPIcs, Vol.6, 2010.
(紹介者：齋藤,2021/12/23)
V. van Oostrom, Z; Syntax-Free Developments, In Proc. of 6th FSCD, pp.24:1--24:22, LIPIcs, Vol.195, 2021.
(紹介者：笠鳥,2021/12/16)
嶌津聡志, 青戸等人, 外山芳人, 反証機能付き書き換え帰納法のための補題自動生成法, コンピュータソフトウェア, Vol.26, No.2, pp.41-55, 2009.
(紹介者：東,2021/12/14)
H． Zankl, B． Felgenhauer, A． Middeldorp, Labelings for Decreasing Diagrams, Journal of Automated Reasoning, Vol.54(2), pp.101-133, 2015.
(紹介者：櫻井,2021/12/9)
K. Kikuchi and T. Aoto, Simple derivation systems for proving sufficient completeness of non-terminating term rewriting systems, In Proc. of 41st FSTTCS, LIPIcs Vol.213, pp.49:1-49:15, 2021.
(紹介者：冨田,2021/12/2)
大堀淳，上野雄大， SML#で始める実践MLプログラミング，共立出版，2021．(の7章と11章)
(紹介者：渋谷,2021/11/25)
A． K． Eeralla and C． Lynch, Bounded ACh unification, Mathematical Structures in Computer Science, Vol.30(6), pp.664-682, 2020.
(紹介者：井出,2021/11/11)
N． Nishida and G． Vidal, Conversion to tail recursion in term rewriting, Journal of Logic and Algebraic Programming, Vol.83(1), pp.53-63, 2014.
(紹介者：渡辺,2021/11/4)
鈴木翼, 青戸等人, 外山芳人, 永続性に基づく項書き換えシステムの合流性証明法コンピュータソフトウェア, Vol.30, No.3, pp.148-162, 2013.
(紹介者：趙，2021/10/14,21)
G.Godoy and F.Jacquemard, Unique Normalization for Shallow TRS, In Proc. of 20th RTA, LNCS, Vol.5595, pp.63-77, 2009.
(紹介者：望月，2021/7/15,29)
M.Ishizuka, T.Aoto and M.Iwami, Commutative rational term rewriting, In Proc. of 15th LATA, LNCS, Vol.12638, 2021,pp.200-212, 2021.

2020年度

輪講

(2020/4/30開始，2021/2/10終了，2章まで)
Michael R. A. Huth, Mard D. Ryan, Logic in Computer Science: Modelling and reasoning about systems, Cambridge University Press, 2nd edition, 2004.
参加者：趙，望月，渡邉，長橋，深谷，大野，芳賀(り)，宮前
(2020/4/30開始，2021/2/10終了，8章まで))
Paul Chiusano, Runar Bjarason, Fuctional Programming in Scala, Manning Publication, 2014.
参加者：冨田，芳賀(ま)，南山，笹川，佐藤，西野，波多野，宮前
(2017/11/29開始，継続中)
Steve Awodey, Category Theory, Oxford University Press, 2010.
参加者：宮前，高橋，青戸

論文(解説)紹介

(紹介者：芳賀(雅)，2021/1/28)
Mauricio Ayala-Rincon, M. Fernández and Daniele Nantes-Sobrinho, On nominal syntax and permutation fixed points, Logical Methods in Computer Science, Vol.16, No.1, 2020, pp.19:1-19:36.
(紹介者：南山，2021/1/22)
Dexter Kozen and Alexandra Silva, Practical coinduction, Mathematical Structures in Computer Science, Vol.27, No.7, pp.1132-1152, 2017.
(紹介者：芳賀(亮)，2021/1/21)
加賀谷有輝, 青戸等人, 条件付き項書き換えシステムの階層合流性証明法, 第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集, 2020.
(紹介者：長橋，2020/12/24)
Keisuke Nakano, Shall We Juggle, Coinductively?, In Poceedings of the 2nd International Conference on Certified Programs and Proofs (CPP 2012), Lecture Notes in Computer Science, vol.7679, 2012Springer-Verlag.
(紹介者：望月，2020/12/17,23)
Takahito Aoto and Jeroen Ketema, Rational term rewriting revisited: decidability and confluence, In Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012), Bremen, Germany, September 2012, pp.172-186, Lecture Notes in Computer Science, Vol.7562, Springer-Verlag.
(紹介者：渡邊，2020/12/10)
Takahito Aoto and Yoshihito Toyama, Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems, In Proc. of 12th FroCoS, 2019, pp.330-347, LNAI, Vol.11715, Springer-Verlag.
(紹介者：深谷，2020/12/3)
Takahito Aoto and Yoshihito Toyama, Ground confluence prover based on rewriting induction, In Proc. of 1st FSCD, LIPIcs, Vol. 52, pp.33:1-33:12, 2016.
(紹介者：冨田，2020/11/26)
篠埜功,大堀淳, SML♯へのC言語の埋め込み, コンピュータソフトウェア, Vol. 29, No. 2, pp.193-203, 2012．
(紹介者：趙，2020/11/12)
M. Fernández and M.J. Gabbay, Nominal rewriting, Information and Computation, Vol.205, pp.917-965, 2007.
(紹介者：芳賀(雅)，2020/8/4)
Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama. Critical pair analysis in nominal rewriting, In Proc. of 7th SCSS, EPiC Series in Computing, Vol.39, EasyChair, 2016, pp.156-168.
(紹介者：大野，2020/7/20)
S. Winkler, R. Thiemann, Formalizing soundness and completeness of unravelings, In Proc. of 10th FroCoS, LNCS, Vol.9322, Springer-Verlag, 2015, pp.239-255.
(紹介者：芳賀(雅)，2020/6/10,25)
James Brotherston, Nikos Gorogiannis, Rasmus L. Petersen, A Generic Cyclic Theorem Prover, In Proc. of 10th APLAS, 2012, pp.350-367, LNCS, Vol.7705, Springer.
(紹介者：南山，2020/6/10,15,25)
G. Roşu and D. Lucanu, Circular Coinduction: A Proof Theoretical Foundation. In Proceedings of 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO), LNCS, Vol.5728. pp.127-144, 2009.
(紹介者：芳賀(亮)，2020/6/1)
Karl Gmeiner, Confluence of Conditional Term Rewrite Systems via Transformations, In Proceedings of WPTE 2016, EPTCS 235, 2017, pp. 32-45.
(紹介者：大野，2020/5/13)
Karl Gmeiner, Naoki Nishida and Bernhard Gramlich, Proving confluence of conditional term rewriting systems via unravelings, In Proceedings of 2nd IWC, pp.35-40, 2012.

2019年度

輪講

(2019/4/25開始，2020/1/7終了，C章まで) D.C. Kozen, Automata and Computability, Springer, 1997.
参加者：大野，岡本，芳賀(雅)，芳賀(亮)，南山，笹川，佐藤，石塚，加賀谷，白石，東和田，山口，青戸
(2019/4/25開始，2020/1/27終了，2章まで)
M. Barr, C. Wells, Category Theory for Computer Science, Reprints in Theory and Applications of Categories, No.22, 2012.
参加者：風間，芳賀(雅)，佐藤，西野，宮前，青戸
(2017/11/29開始，継続中)
Steve Awodey, Category Theory, Oxford University Press, 2010.
参加者：宮前，高橋，青戸

論文(解説)紹介

(紹介者：佐藤，2019/7/31)
Rakesh Verma, New Undecidability Results for Properties of Term Rewrite Systems, Electronic Notes in Theoretical Computer Science, Vol.290, pp.69-85, 2012.
(紹介者：笹川，2019/7/10,24)
J.A. Bergstra and J.W. Klop, Conditional rewrite rules: Confluence and termination, Journal of Computer and System Sciences, Vol.32, No.3, pp.323-362, 1986.
(紹介者：宮前，2019/7/10,17)
G. Roşu and D. Lucanu, Circular Coinduction: A Proof Theoretical Foundation. In Proceedings of 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO), LNCS, Vol.5728. pp.127-144, 2009.
(紹介者：西野，2019/7/3)
Adrien Ycart, Florent Jacquemard, Jean Bresson, Slawomir Staworko. A Supervised Approach for Rhythm Transcription Based on Tree Series Enumeration, In Proceedings of the 42nd International Computer Music Conference (ICMC), Sep 2016, Utrecht, Netherlands.
(紹介者：宮前，2019/6/12)
B. Jacobs, J. Rutten, An introduction to (co)algebra and (co)induction. In Advanced Topics in Bisimulation and Coinduction, pp.38-99, 2011, Cambridge University Press.
(紹介者：佐藤，2019/6/10)
I. Mitsuhashi, M. Oyamaguch and F. Jacquemard, The Confluence Problem for Flat TRSs, Proc. of 8th AISC, LNAI 4120, pp.68-81, 2006, Springer-Verlag.

2018年度

輪講

(2018/4/26開始，2019/2/8終了，7章まで)
Glynn Winskel, The Formal Semantis of Programming Languages - An Introduction, The MIT Press, 1993.
参加者：清水，西野，山口(真)，白石，東和田，山口(諒)，加藤，木村，萩原，青戸
(2018/4/26開始，2019/2/12終了，3章まで)
B.A. Davey, H.A. Priestley, Introduction to Lattices and Order, 2nd ed. Campbridge University Press, 2002.
参加者：笹川，佐藤，(下平〜2018前期)，山口(真)，石塚，加賀谷，加藤，栗田，新山，青戸
(2017/11/29開始，継続中)
Steve Awodey, Category Theory, Oxford University Press, 2010.
参加者：加藤，萩原，宮前，高橋，青戸

論文(解説)紹介

(紹介者：西野，2018/12/10)
Y. Toyama, Termination proof of S-expression Rewrite Systems with Recursive Path Relations, In Proceeding of 19th RTA, LNCS, Vol.5117, pp.381–391, 2008
(紹介者：東和田，2018/12/3)
Christian Sternagel and Thomas Sternagel, Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems, In Proceedings of CADE 2017, LNAI 10395, pp.413-431, 2017
(紹介者：佐藤，2018/11/26, 2018/12/17)
J.-P. Jouannaud and H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM Journal on Computing, Vol.15, No.4, pp.1155-1194, 1986
(紹介者：清水，2018/11/16)
T. Nipkow, Functional unification of higher-order patterns, In Proceedings of 8th LICS, pp.64-74, 1993, ACM.
(紹介者：笹川，2018/11/9)
Nao Hirokawa, Aart Middeldorp, Harald Zankle, Uncurrying for Termination and Complexity Journal Automated Reasoning, Vol.50, pp.279-315, 2013.
(紹介者：山口(真)，2018/10/26)
Nicholas R. Radcliffe, Luis F. T. Moraes and Rakesh M. Verma, Uniqueness of normal forms for shallow term rewrite systems. ACM Transactions on Computational Logic, Vol.18, No.2, 17, 2017,
(紹介者：加賀谷，2018/10/19)
Taro Suzuki, Aart Middeldorp and Tetsuo Ida, Level-confluence of conditional rewrite systems with extra variables in right-hand sides, In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA 1995), LNCS Vol.914, pages 179–193, 1995, Springer-Verlag.
(紹介者：石塚，2018/10/12)
Takahito Aoto and Jeroen Ketema, Rational term rewriting revisited: decidability and confluence, In Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012), Bremen, Germany, September 2012, pp.172-186, Lecture Notes in Computer Science, Vol.7562, Springer-Verlag.
(紹介者：白石，2018/6/27)
Yoshihito Toyama, How to prove equivalence of term rewriting systems without induction, Theoretical Computer Science, Vol.90, pp.369-390, 1991.
(紹介者：山口，2018/6/13)
P. Urso and E. Kounalis, "Term partition" for mathematical induction, In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA 2003), LNCS, vol.2706, pp.352–366, 2003, Springer-Verlag.
(紹介者：加藤，2018/5/22)
Nishida N. and Vidal G., A Finite Representation of the Narrowing Space, In Proceedings of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013), Lecture Notes in Computer Science, Vol. 8901, pp.54-71, 2013, Springer-Verlag.
(紹介者：加賀谷，2018/5/15)
Yoshihito Toyama, Commutativity of term rewriting systems, In K. Fuchi and L. Kott, eds., Programming of Future Generation Computer II, pp.393-407, North-Holland, Amsterdam, 1988.
(紹介者：石塚，2018/5/9)
Joxan Jaffer, Efficient Unification over Infinite Terms, New Generation Computing, Vol.2, No.3, pp.207-219, 1984.
(紹介者：白石，2018/4/15)
小池広高，外山芳人，潜在帰納法と書換え帰納法の比較，コンピュータソフトウェア，Vol.17, No.6, pp.1-12, 2000.

2017年度

輪講

(2017/4/21開始，2018/2/23終了，4章まで)
Jean H. Gallier, Logic for Computer Science, Oover Publications, 1986.
参加者：石塚，泉田，加賀谷，白石，瀬木，山口，加藤，木村，栗田，新山，萩原，青戸
(2017/5/15開始，2017/7/24終了，2章まで)
Uwe Schoning, Jacobo Toran, The Satisfiability Problem, Lehmanns Media, 2013.
参加者：Tobias，加藤，木村，栗田，萩原，青戸
(2017/11/29開始，継続中)
Steve Awodey, Category Theory, Oxford University Press, 2010.
参加者：加藤，萩原，宮前，高橋，青戸

論文(解説)紹介

(紹介者：石塚, 2017/11/13)
Chapter 10 of Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 223-265，1998.
(紹介者：山口, 2017/11/16)
T. Aoto and S. Stratulat. Decision procedures for proving inductive theorems without induction. In Proc. of 16th PPDP, pages 237–248. ACM Press, 2014.
(紹介者：白石, 2017/11/20)
Takahito Aoto, Yoshihito Toyama and Yuta Kimura, Improving Rewriting Induction Approach for Proving Ground Confluence, In Proc. of 2nd FSCD, pp.7:1--7:18, LIPIcs, 2017.
(紹介者：加賀谷, 2017/11/27)
Leo Bachmair, Nachum Dershowitz and David A. Plaisted, Completion without Failure, In Resolution of Equations in Algebraic Structures, Academic Press, Vol.2, pp.1-30, 1989.
(紹介者：泉田, 2017/11/30)
山田俊行，Aart Middeldorp, 井田哲雄，条件付き項書換え系における階層合流性のモジュラ性, コンピュータソフトウェア，Vol.12, No.5, pp.72-84, 1995.
(紹介者：瀬木, 2017/12/4)
Sections 7.1/7.3 of Franz Baader and Tobias Nipkow, Advanced Topics in Term Rewriting, Cambridge University Press, 1998.
(紹介者：石塚, 2017/12/11)
岩見宗弘, 青戸等人, 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証, コンピュータソフトウェア, Vol.29, No.1, pp.211-239, 2012．
(紹介者：新山，2017/7/12)
Congurence closure, Section 4.3 of Franz Baader, Tobias Nipkow, Term Rewriting and All That, Cambridge University, 1998.
(紹介者：木村，2017/7/5)
Nao Hirokawa and Aart Middeldorp. Tyrolean termination tool: Techniques and features. Information and Computation, 205(4):474 – 511, 2007.
(紹介者：萩原，2017/6/1)
Ursula Martin and Tobias Nipkow, Ordered Rewriting and Confluence, CADE-10 Proceedings of the tenth international conference on Automated deduction, pp.366-380, 1990.
(紹介者：新山，2017/5/18)
Yoshihito Toyama and Michio Oyamaguchi, Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems, Springer-Verlag, 1995.
(紹介者：木村，2017/5/10)
Matsahito Kurihara and Hisashi Kondo, Completion for Multiple Orderings, Journal of Automated Reasoning 23(1): 25-42, 1999.
(紹介者：栗田，2017/4/26, 2017/5/1)
Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems,
(紹介者：加藤，2017/4/20)
Clessen K., Johansson M., Rosen D., Smallbone N. (2013) Automating Inductive Proofs Using Theory Exploration. In: Bonacina M.P. (eds) Automated Deduction - CADE-24. CADE 2013. Lecture Notes in Computer Science, vol 7898. Springer, Berlin, Heidelberg.

2016年度

輪講

(2016/4/28開始，2017/3/3終了，読了)
Maribel Fernandez, Programming Languages and Operational Semantics, Springer, 2014.
参加者：加藤，木村，栗田，新山，萩原，青戸

論文(解説)紹介

(紹介者：木村，2017/1/17)
Ian Wehrman, Aaron Stump and Edwin Westbrook, Slothrop: Knuth-Bendix completion with a modern termination checker， In Proc. of 17th RTA, LNCS 4098, Springer-Verlag, 2006.
(紹介者：新山，2017/1/10)
濱口毅, 酒井正彦, 馬場正貴, 阿草清滋, 例外処理を持つ関数型プログラムの停止性・非停止性証明法, 情報処理学会論文誌プログラミング, Vol.4, No.2, pp.13-30, 2011.
(紹介者：萩原，2016/12/19)
Leo Bachmair and Nachum Dershowitz and David A. Plaisted, Completion without failure, In Resolution of Equation in Algebraic Structure, pp.31-86, 1989, Academic Press.
(紹介者：加藤，2016/12/13)
Deepak Kapur and M.Subramaniam, Lemma Discover in Automating Induction, In Proc. of CADE-13, LNAI 1104, pp.538-552, 1996, Springer.
(紹介者：栗田，2016/11/29)
Sarah Winkler and René Thiemann, Formalizing soundness and completeness of unravelings, In Proc. of 10th FroCoS, LNCS 9322, pp. 239-255, 2015.
(紹介者：新山，2016/11/15)
大堀淳, LR構文解析の原理, コンピュータソフトウェア, Vol.31, No.1, pp.30-42, 2013.
(紹介者：萩原，2016/11/1)
Dominik Klein and Nao Hirokawa, Maximal completion, In Proc. of 22nd RTA, pp. 71-80, LIPIcs, Vol.10, 2011.
(紹介者：木村，2016/10/25)
Takahito Aoto and Yoshihito Toyama, Ground confluence prover based on rewriting induction, In Proc. of 1st FSCD, LIPIcs, Vol. 52, pp.33:1--33:12, 2016.
(紹介者：加藤，2016/10/18)
嶌津聡志, 青戸等人, 外山芳人, 反証機能付き書き換え帰納法のための補題自動生成法, コンピュータソフトウェア, Vol.26, No.2, pp.41-55, 2009.