Program
September 16
| 14:00 – 15:30 | Session 1 (chair: N. Nishida) |
14:00|
On Transforming Prioritized Multithreaded Programs into Logically Constrained Term Rewrite Systems |
Misaki Kojima Nagoya U. |
14:45|
Ground-Total Generalization of Weighted Path Order |
Teppei Saito JAIST |
| 15:30 – 16:00 | Break |
| 16:00 – 17:30 | Session 2 (chair: M. Kojima) |
16:00|
Confluence Analysis by Rule Removal |
Fuyuki Kawano JAIST |
16:45|
Improving Confluence Analysis for Logically Constrained Rewrite Systems |
Aart Middeldorp U. Innsbruck |
September 17
| 10:00 – 11:30 | Session 3 (chair: A. Middeldorp) |
10:00|
Disproving Termination of S-like Combinators by Tree Automata
|
Munehiro Iwami Iwate Prefectural U. |
11:00|
Quantitative Extensions of Rewriting |
Akihisa Yamada AIST |
| 11:30 – 13:30 | Lunch Break |
| 13:30 – 15:00 | Session 4 (chair: M. Iwami) |
13:30|
An Equational Unification Tool |
Nao Hirokawa JAIST |
14:15|
Exploring Large Language Models for Coq Theorem Proving |
Hideto Kasuya Aichi Prefectural U. |
| 15:00 – 15:30 | Break |
| 15:30 – 17:00 | Session 5 (chair: A. Yamada) |
15:30|
Formalization of Component-Based Projected Model Counting Method |
Kenta Ito Nagoya U. |
16:00|
Towards Confluence of Deterministic Higher-Order Pattern Rewrite Systems by Critical Pairs |
Aart Middeldorp U. Innsbruck |
| 17:00 – 17:30 | Business Meeting |
September 18
| 10:00 – 11:30 | Session 6 (chair: N. Hirokawa) |
10:00|
A recursive function to enumerate canonical systems of a ground TRS |
Masahiko Sakai Nagoya U. |
10:45|
Difference of Constrained Terms in LCTRSs |
Naoki Nishida Nagoya U. |
| 11:30 – 12:00 | Closing |