51st TRS Meeting

September 25 – 27, 2019
Sōunkyō, Hokkaido, Japan

Program

September 25

14:30 – 15:00 Registration
15:00 – 15:05 Opening
15:05 – 17:00 Session 1 (chair: T. Aoto)
15:05 On Inversion and Determinization via Context-Free Expressions
Naoki Nishida Nagoya U.
15:55 On Formalizing Logically Constrained TRSs in Isabelle/HOL
Ryota Nakayama Nagoya U.
16:30 Simplification of ROBDD Generated by Binary Base Form Pseudo-Boolean Constraints
Jiaqi He Nagoya U.

September 26

9:00 – 10:35 Session 2 (chair: N. Nishida)
9:00 An Extension of the Parallel Closedness Theorem
Kiraku Shintani JAIST
9:50 Termination in FORT: Infinity Predicate Formalization
Aart Middeldorp U. Innsbruck
10:35 – 10:50Break
10:50 – 12:00 Session 3 (chair: K. Nakazawa)
10:50 Comparison of Uniform Semi-Unification and Rational Unification Revisited
Munehiro Iwami Shimane U.
11:25 Rhythm quantization as an efficiently-solvable optimization problem
Masahiko Sakai Nagoya U.
12:00 – 14:00Lunch Break
14:00 – 15:15 Free Discussion
15:15 – 15:30Break
15:30 – 17:00 Free Discussion

September 27

9:00 – 10:35 Session 4 (chair: A. Middeldorp)
9:00 On Proving Termination of Bit-Vector LCTRSs
Donghoon Shin Nagoya U.
9:35 Productivity in Finitary Rewriting
Akihisa Yamada NII
10:20 – 10:35Break
10:35 – 12:00 Session 5 (chair: M. Iwami)
10:35 Development Closedness and Proofclusters
Nao Hirokawa JAIST
11:10 Level-Confluence of Left-Linear Overlapping CTRSs
Takahito Aoto Niigata U.
12:00 – 14:00Lunch Break
14:00 – 15:05 Session 6 (chair: A. Yamada)
14:00 Commutative Rewrite Steps in Rational Term Rewriting
Mamoru Ishizuka Niigata U.
14:35 On Cut-Elimination in Cyclic-Proof System
Koji Nakazawa Nagoya U.
15:05 – 15:20Break
15:20 – 16:50 Session 7 (chair: N. Hirokawa)
15:20 Confluence Proof of λμ Calculus by Z Theorem
Yuuki Honda Nagoya U.
15:55 A Simple Proof for Kahrs-Smith's Theorem
Michio Oyamaguchi Nagoya U.
16:30 – 16:50 Business Meeting
16:50 – 17:00 Closing