49th TRS Meeting

25 -- 27 September 2018, Ikaho (Gunma)

Term Rewriting Meeting (TRS Meeting) is a biannual informal workshop that aims at promoting the research on rewriting and related areas. Participants are requested to give a talk(s) of approximately 15 - 60 minutes in English on their research activities. See also Rewriting Researchers Forum for further information. We should like to invite all of you to the upcoming TRS Meeting at Ikaho, Gunma.

• Date: September 25 (Tues) -- 27 (Thur), 2018

• Venue: Ikaho Onsen, Nagomigokoro No Yado Omori, Entrance and meeting room

  58 Ikaho, Shibukawa city, Gunma 371-0102

• Access: See http://www.ikaho-omori.com/eng/

• Schedule

  Opening: 14:00 on Sept 25 (Tues)

  Closing: 12:00 on Sept 27 (Thur)

• Fee

  Registration for meeting room fee: 4,000 JPY

  Accommodation fee including breakfasts and dinners (lunches are not included):

  A shared room with three (11,490 JPY per night)

  (A six-mat single room (12,030 JPY per night) but limited to several)

• Map for lunch around THE Stone Steps

• Registration form

  Please send the registration form below to Ken-etsu Fujita (mailto: fujita at cs.gunma-u.ac.jp) no later than August 24, 2018. Registration after the deadline is subject to room availability.

-------------------------------------------------------------------------------------------------------------

Registration Form of the 49th TRS meeting

• Name:
• Affilation:
• [male / female] (leave one)
• special room request: [single room / shared room / none] (leave one)
• Title of talk:
• Approximate duration of talk in minutes (between 15 and 60):

Japanese style shared rooms are default, but several single are also available. If you prefer a single, let me know at your earliest convenience (* Now NO single roomes *). In the latter case, let me also know your roommate.

Ken-etsu Fujita (mailto: fujita at cs.gunma-u.ac.jp)

• Takahito Aoto (Niigata Univ.)
• Ken-etsu Fujita (Gunma Univ.)
• Nao Hirokawa (JAIST)
• Munehiro Iwami (Shimane Univ.)
• Hiroto Kato (Niigata Univ.)
• Yuta Kimura (Niigata Univ.)
• Taichi Kurita (Niigata Univ.)
• Aart Middeldorp (University of Innsbruck)
• Hiromu Niiyama (Niigata Univ.)
• Naoki Nishida (Nagoya Univ.)
• Michio Oyamaguchi (Nagoya Univ.)
• Masahiko Sakai (Nagoya Univ.)
• Christian Sternagel (University of Innsbruck)
• Kiraku Shintani (JAIST)
• Akihisa Yamada (NII)

Sept 25 (Tues), 2018

14:15 -- 16:50 (Chairman: Aart Middeldorp)

• 14:15--15:00 Takahito Aoto (Niigata University):
  Proving Local Sufficient Completeness

• 15:00--15:45 Ken-etsu Fujita (Gunma University):
  A Formal System of Reduction Paths for Parallel Reduction

  break

• 16:00--16:20 Yuta Kimura (Niigata University):
  Formalizing Rewriting Induction in Isabelle/HOL

• 16:20--16:50 Nao Hirokawa (JAIST):
  Moc: New First-Order Theorem Prover

Sept 26 (Wed), 2018

9:30 -- 11:55 (Chairman: Takahito Aoto)

• 9:30--10:15 Munehiro Iwami (Shimane University):
  Relational Unification Modulo Rewriting System

• 10:15--10:35 Hiroto Kato (Niigata University):
  Lemma Generation Methods for Inductive Theorem Proving

  break

• 10:50--11:10 Hiromu Niiyama (Niigata University):
  Automatic verification of Unique normalizability of Term Rewriting System

• 11:10--11:55 Naoki Nishida (Nagoya University):
  Proving Infeasibility by Narrowing Tree

14:10 -- 16:45 (Chairman: Munehiro Iwami)

• 14:10--14:55 Christian Sternagel (University of Innsbruck):
  Reachability Analysis for CTRS's in ConCon

• 14:55--15:25 Kiraku Shintani (JAIST):
  Confluence for left-linear composable systems

  break

• 15:40--16:00 Taichi Kurita (Niigata University):
  Automated proofs of Horn-clause Inductive Theorems for CTRS

• 16:00--16:45 Aart Middeldorp (University of Innsbruck):
  A Verified Ground Confluence Tool for Linear-Variable-Separated Rewrite Systems in Isabelle/HOL

Sept 27 (Thur), 2018

9:30 -- 12:00 (Chairman: Nao Hirokawa)

• 9:30--10:15 Akihisa Yamada (NII):
  Relational Differential Dynamic Logic

• 10:15--11:00 Masahiko Sakai (Nagoya University):
  An extended SQL for combinatorial optimization problems and transformation into constraint problems

  break

• 11:15--12:00 Michio Oyamaguchi (Nagoya University):
  Is a Simple Proof Possible for Kahrs-Smith's Theorem?

• First step
• 50 < step < 200 : Target; Closed; GarbageStation; Food; BlindAlley; BowArrow; WindBell
• 200th step : Yosano Akiko
• 200 < step < 365 : Restrant-Liquor; Post; WindBell; BagShop; Shop; Map
• A flight of 365 steps of stairways leading to Ikaho Shrine