General Information
Nao Hirokawa (associate professor)
Contact
- address:
- School of Information Science
Graduate School of Advanced Science and Technology
Japan Advanced Institute of Science and Technology
1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan
- office:
- I-54a (on 5th floor of Information Science Building II)
- phone:
- +81-761-51-1277
- email:
- hirokawa
term rewriting
@jaist.ac.jp
- research group:
- Hirokawa Laboratory
- research interests:
- computational models (term rewriting, automata, complexity analysis)
automated deduction (automated theorem proving, SAT/SMT solving)
Maxcomp and Moca
Saigawa
Teaching
Upcoming Events
-
24th International
Conference on Logic for Programming, Artificial Intelligence and
Reasoning (LPAR-24), June 4 - 9, 2023, Manizales Colombia.
-
8th International
Conference on Formal Structures of Computation and Deduction (FSCD 2023), July 3 - 6,
2023, Rome, Italy.
-
29th International
Conference on Automated Deduction (CADE-29), July 1 - 4,
2023, Rome, Italy.
Research Activities
Steering Committee Member
- IWC (2011-2020)
- International Workshop on Confluence
- CoCo (2011-2018)
- Confluence Competition
- LCC (2015-2017)
- International Workshop on Logic and Computational Complexity
- FSCD (2015-2016)
- International Conference on Formal Structures of Computation and Deduction
- RTA (2014-2015)
- International Conference on Rewriting Techniques and Applications (RTA)
Program Committee Member
- LPAR-24
- 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
- CADE-29
- 29th International Conference on Automated Deduction
- FSCD 2023
- 8th International Conference on Formal Structures of Computation and Deduction
- WRLA 2022
- 14th International Workshop on Rewriting Logic and its Applications,
- CADE-28
- 28th International Conference on Automated Deduction
- PPL 2021
- 23rd Workshop on Programming and Programming Languages
- LPAR-23
- 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
- FSCD 2020
- 5th International Conference on Formal Structures of Computation and Deduction
- WRLA 2020
- 13th International Workshop on Rewriting Logic and its Applications
- FLOPS 2020
- 15th International Symposium on Functional and Logic Programming
- PPL 2020
- 22nd Workshop on Programming and Programming Languages
- CADE-27
- 27th International Conference on Automated Deduction
- FSCD 2019
- 4th International Conference on Formal Structures of Computation and Deduction
- DICE-FOPARA 2017
- 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis
- ITP 2017
- 8th International Conference on Interactive Theorem Proving
- FSCD 2016
- 1st International Conference on Formal Structures of Computation and Deduction
- IWC 2016
- 5th International Workshop on Confluence
- CADE-25
- 25th International Conference on Automated Deduction
- PEPM 2015
- Workshop on Partial Evaluation and Program Manipulation
- LCC 2015
- 16th
International Workshop on Logic and Computational Complexity, co-chair
- PPL 2014
- 16th Workshop on Programming and Programming Languages
- SCSS 2014
- 6th International Symposium on Symbolic Computation in Software Science
- LPAR-19
- 19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning
- RTA 2013
- 24th International Conference on Rewriting Techniques and Applications
- IWC 2013
- 2nd International Workshop on Confluence,
co-chair
- DCM 2013
- 9th International Workshop on Developments in Computational Models
- WST 2013
- 13th International Workshop on Termination
- RTA 2012
- 23rd International Conference on Rewriting Techniques and Applications
- IWC 2012
- 1st
International Workshop on Confluence, co-chair
- WST 2012
- 12th International Workshop on Termination
- DICE 2012
- 3rd International Workshop on Developments in Implicit Complexity
Organization
- AJSW 2016
- 4th Austria
- Japan Summer Workshop on Term Rewriting
- JL 2014
- 1st JAIST-LORIA Workshop
- PR 2013
- 3rd Workshop on Proof Theory and Rewriting
Memberships
- IFIP TC1
- IFIP Technical Committee 1
(Foundations of Computer Science), 2018-
- IFIP WG 1.6
- IFIP Working Group 1.6
(Rewriting), 2014-
Publications
Journal Articles
- LMCS 2019
- Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler.
Abstract Completion, Formalized
Journal of Logical Methods in Computer Science, 15(3):1:1-1:19, 2019.
doi: 10.23638/LMCS-15(3:19)2019
errata
- TPLP 2016
- Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp.
AC-KBO Revisited,
Theory and Practice of Logic Programming, 16(2):163-188,
2016.
- JAR 2013
- Nao Hirokawa, Aart Middeldorp, and Harald Zankl.
Uncurrying for Termination and
Complexity
Journal of Automated Reasoning 50(3):279-315, 2013.
- JAR 2011
- Nao Hirokawa and Aart Middeldorp
Decreasing
Diagrams and Relative Termination
Journal of Automated Reasoning 47(4):481-501, 2011
- JAR 2009
- Harald Zankl, Nao Hirokawa, and Aart Middeldorp
KBO Orientability
Journal of Automated Reasoning 43(2):173-201, 2009
- IC 2007
- Nao Hirokawa and Aart Middeldorp
Tyrolean
Termination Tool: Techniques and Features
Information and Computation 205(4):474-511, 2007
- IC 2005
- Nao Hirokawa and Aart Middeldorp
Automating the
Dependency Pair Method
Information and Computation 199(1,2):172-199, 2005
Conference and Workshop Papers
- FSCD 2023
-
Nao Hirokawa and Aart Middeldorp
Hydra Battles and AC Termination
Proceedings of the 8th International Conference on Formal
Structures for Computation and Deduction, Leibniz International
Proceedings in Informatics, 2023.
doi: tba
- FSCD 2022
-
Kiraku Shintani and Nao Hirokawa
Compositional Confluence Criteria
Proceedings of the 7th International Conference on Formal
Structures for Computation and Deduction, Leibniz International
Proceedings in Informatics, 2022.
doi: 10.4230/LIPIcs.FSCD.2022.28
- FSCD 2021
-
Nao Hirokawa
Completion and Reduction Orders
Proceedings of the 6th International Conference on Formal
Structures for Computation and Deduction, Leibniz International
Proceedings in Informatics 195, pp. 2:1-2:9, 2021.
doi: 10.4230/LIPIcs.FSCD.2021.2
errata
slides
- CADE 2019
-
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, and Michio
Oyamaguchi
Confluence by Critical Pair Analysis Revisited
Proceedings of the 27th International Conference on Automated
Deduction, Lecture Notes in Computer Science 11716, pp. 319-335, 2019.
doi: 10.1007/978-3-030-29436-6_19
extended version
- FSCD 2018
-
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian
Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl
Confluence Competition
2018
Proceedings of the 3rd International Conference on Formal
Structures for Computation and Deduction, Leibniz International
Proceedings in Informatics 108, pp. 32:1-32:5, 2018
- IJCAR 2018
-
Nao Hirokawa, Julian Nagele, and Aart Middeldorp
Cops and CoCoWeb: Infrastructure for Confluence Tools
Proceedings of the 9th International Joint Conference on Automated
Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 346-353, 2018
doi: 10.1007/978-3-319-94205-6_23
- FSCD 2017
- Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler
Infinite Runs in Abstract Completion
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:1--19:16, 2017.
- CADE 2015
- Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and
Harald Zankl
Confluence Competition
2015
Proceedings of the 25th International Conference on Automated
Deduction, Lecture Notes in Artificial Intelligence 9195, pp. 101-104,
2015.
- CADE 2015
- Kiraku Shintani and Nao Hirokawa
CoLL: A Confluence Tool for
Left-Linear Term Rewrite Systems
Proceedings of the 25th International Conference on Automated
Deduction, Lecture Notes in Artificial Intelligence 9195, pp. 127-136,
2015.
- RTA 2015
-
Nao Hirokawa, Aart Middeldorp, and Georg Moser
Leftmost Outermost
Revisited
Proceedings of the 26th International Conference on Rewriting
Techniques and Applications, Leibniz International Proceedings in
Informatics 36, pp. 209-222, 2015.
- RTA-TLCA 2014
-
Nao Hirokawa and Georg Moser
Automated Complexity
Analysis Based on Context-Sensitive Rewriting
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications
and 12th International Conference on Typed Lambda Calculi and Applications,
Lecture Notes in Computer Science 8560, pp. 257-271, 2014.
- ITP 2014
-
Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
A New and Formalized Proof of
Abstract Completion
Proceedings of the 5th International Conference on Interactive Theorem Proving,
Lecture Notes in Computer Science 8558, pp. 292-307, 2014.
- FLOPS 2014
-
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
AC-KBO Revisited
Proceedings of the 12th International
Symposium on Functional and Logic Programming, Lecture Notes in Computer
Science 8475, pp. 319-335, 2014.
- LPAR 2012
-
Dominik Klein and Nao Hirokawa
Confluence of Non-Left-Linear
TRSs via Relative Termination
Proceedings of the 18th International
Conference on Logic for Programming, Artificial Intelligence and Reasoning,
Lecture Notes in Computer Science 7180, pp. 258-273, 2012.
- RTA 2011
-
Dominik Klein and Nao Hirokawa
Maximal Completion
Proceedings of the 22nd International
Conference on Rewriting Techniques and Applications, Leibniz International
Proceedings in Informatics 10, pp. 71-80, 2011.
In the above PDF numbers 2, 5, and 14 for
K (on pages 7 and 9) were corrected to 1, 4, and 13, respectively.
- HOR 2010
-
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Uncurrying
for Innermost Termination and Derivational Complexity
Proceedings of the 5th International
Workshop on Higher-Order Rewriting, Electronic Proceedings in Theoretical
Computer Science 49, pp. 46-57, 2011
- IJCAR 2010
-
Nao Hirokawa and Aart Middeldorp
Decreasing Diagrams and Relative
Termination
Proceedings of the 5th International Joint
Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence
6173, pp. 487-501, 2010
- LPAR 2008
-
Nao Hirokawa, Aart Middeldorp, and Harald Zankl
Uncurrying for Termination
Proceedings of the 15th International Conferences on Logic for
Programming, Artificial Intelligence and Reasoning, Lecture Notes in
Computer Science 5330, pp. 667-681, 2008
- LPAR 2008
-
Nao Hirokawa and Georg Moser
Complexity, Graphs, and the Dependency Pair
Method
Proceedings of the 15th International Conferences on Logic for
Programming, Artificial Intelligence and Reasoning, Lecture Notes in
Computer Science 5330, pp. 652-666, 2008
errata
- IJCAR 2008
-
Nao Hirokawa and Georg Moser
Automated Complexity Analysis Based on the Dependency
Pair Method
Proceedings of the 4th International Joint Conference
on Automated Reasoning, Lecture Notes in Artificial Intelligence 5195,
pp. 364-379, 2008
errata
- SOFSEM 2007
-
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Constraints for Argument Filterings
Proceedings of the 33rd International Conference
on Current Trends in Theory and Practice of Computer Science,
Lecture Notes in Computer Science 4362, pp. 579-590, 2007
- RTA 2006
-
Nao Hirokawa and Aart Middeldorp
Predictive
Labeling
Proceedings of the 17th International
Conference on Rewriting Techniques and Applications,
Lecture Notes in Computer Science 4098, pp. 313-327, 2006
- RTA 2005
-
Nao Hirokawa and Aart Middeldorp
Tyrolean
Termination Tool
Proceedings of the 16th International
Conference on Rewriting Techniques and Applications,
Lecture Notes in Computer Science 3467, pp. 175-184, 2005
- AISC 2004
-
Nao Hirokawa and Aart Middeldorp
Polynomial
Interpretations with Negative Coefficients
Proceedings of the 7th International
Conference on Artificial Intelligence and Symbolic Mathematical
Computation, Lecture Notes in Artificial
Intelligence 3249, pp. 185-198, 2004
- RTA 2004
-
Nao Hirokawa and Aart Middeldorp
Dependency
Pairs Revisited
Proceedings of the 15th International
Conference on Rewriting Techniques and Applications, Aachen,
Lecture Notes in Computer Science 3091, pp. 249-268, 2004
- CADE 2003
-
Nao Hirokawa and Aart Middeldorp
Automating
the Dependency Pair Method
Proceedings of the 19th International
Conference on Automated Deduction, Miami, Lecture Notes in
Artificial Intelligence 2741, pp. 32-46, 2003
- RTA 2003
-
Nao Hirokawa and Aart Middeldorp
Tsukuba
Termination Tool
Proceedings of the 14th International
Conference on Rewriting Techniques and Applications, Valencia,
Lecture Notes in Computer Science 2706, pp. 311-320, 2003
errata
Thesis
- Ph.D.
-
Nao Hirokawa
Automated Termination Analysis for Term
Rewriting
Ph.D. Thesis, University of Innsbruck, 2006
Software
- Maxcomp
- A completion tool, which automatically finds a complete term rewrite system for an equational system.
- Saigawa
- A confluence tool for term rewrite systems.
- TTT
- A termination tool for term rewrite systems. This tool is no longer maintained. Instead, I would recommend its more powerful successor TTT2.