52nd TRS Meeting

February 20 (Thu) - 22 (Sat), 2020
Kaga, Ishikawa, Japan


About TRS Meeting

The Term Rewriting Meeting, traditionally called ``TRS Meeting'', is a biannual informal workshop that aims at promoting the research on rewriting and related areas. Participants are encouraged to present their recent activities, observations, and results at the meeting (in English), however, it is perfectly acceptable to explain a paper written by someone else.

Basic Information

February 20 (Thu) - 22 (Sat), 2020
  • Feb 20, 15:00 opening
  • Feb 22, 12:00 closing
Hotel Arrowle
5-1 Shibayama-cho, Kaga, Ishikawa, Japan
Registration Fee:
  • student (full participation): 23,000 JPY
  • non-student (full participation): 25,000 JPY
  • non-student (participation from 21st): 17,000 JPY
The fees cover expenses for a seminar room, refreshments, and banquets on 20th and 21st.
Accommodation Fees:
  • single: 7,850 JPY per night for a single room
  • shared: 6,200 JPY per night for a room shared with two persons
The fees include breakfasts as well as consumption and bathing taxes. Note that neither registration fees nor accommodation fees include costs for lunches.

Registration (closed)

Please send the following registration form to Nao Hirokawa by email. The deadline is January 7 (Tue), 2020.
              Registration Form of the 52nd TRS Meeting


Title of talk (*):
Duration of talk (*):

Preference on your room: [single / shared] 
[Male / Female] (leave one)

Requests/comments (on foods, partial participation, etc.):

The items marked with * can be sent later.


February 20 (Thu)

opening time of the seminar room
15:30 - 17:10
1st session (chair: Nao Hirokawa)
Comparison of Uniform Semi-Unification and Rational Unification Revisited II
Munehiro Iwami
Normalization Analysis via Termination Graphs
Yusuke Suzuki
18:30 - 20:30
20:00 - 21:30
free discussion

February 21 (Fri)

09:00 - 10:20
2nd session (chair: Masahiko Sakai)
The Uniqueness of Normal Forms with Respect to Reductions for Flat Term Rewriting Systems
Yuki Sato
Formalized Constructions in the First-Order Theory of Rewriting
Aart Middeldorp
10:20 - 10:40
coffee break
10:40 - 12:00
3rd session (chair: Munehiro Iwami)
An Isabelle Formalization of Sorted Algebra, Logic, and Constrained Rewriting
Akihisa Yamada
Weighted-Context-Free-Grammar to Produce Parse Tree with Rests and Polyrhythm for Auto Transcription
Kohei Nishino
12:00 - 14:00
lunch break
14:00 - 15:20
4th session (chair: Takahito Aoto)
Mixing Propositional and First Order Quantifiers: Herbrand Expansions and Beyond
Norbert Preining

We construct for every formula A of infinitely valued first order Gödel logic a validity equivalent prenex formula A' with one propositional existential quantifier. A is valid iff A' admits a Herbrand expansion, i.e., a propositionally valid expression.

On Decision Diagrams
Masahiko Sakai
15:20 - 15:40
coffee break
15:40 - 17:00
5th session (chair: Ken-etsu Fujita)
Parallel Closedness and Parallel Critical Pairs
Kiraku Shintani
Parallel Outside Closedness
Nao Hirokawa
18:30 - 20:30
banquet & business meeting
20:30 - 21:30
free discussion

February 22 (Sat)

09:00 - 10:20
6th session (chair: Akihisa Yamada)
George Boolos' "The Hardest Logic Puzzle Ever" Revisited
Fujita Ken-etsu
Proving Sufficient Completeness w.r.t. Reduction of CTRSs Automatically
Takahito Aoto


  1. Takahito Aoto (Niigata University)
  2. Nao Hirokawa (JAIST)
  3. Munehiro Iwami (Shimane University)
  4. Fujita Ken-etsu (Gunma University)
  5. Aart Middeldorp (University of Innsbruck)
  6. Kohei Nishino (Niigata University)
  7. Norbert Preining (Accelia Inc.)
  8. Masahiko Sakai (Nagoya University)
  9. Yuki Sato (Niigata University)
  10. Kiraku Shintani (JAIST)
  11. Yusuke Suzuki (JAIST)
  12. Akihisa Yamada (NII)