Schedule
| Chair: Tetsuo Ida | |
| 09:30-09:45 | Opening |
| 09:45-10:45 | Welcome Talk: An Inductive Inference System and Its Rationality by Wei Li |
| 10:45-11:00 | Tea Break |
| Chair: Arjeh M. Cohen | 11:00-12:00 | Invited Talk: Algebra and Geometry: Interaction Between "Equations" and "Shapes" by Heisuke Hironaka |
| 12:00-14:00 | Lunch |
| Chair: Michael Kohlhase | |
| 14:00-14:30 | Solving Dynamic Geometric Constraints Involving Inequalities by Hoon Hong, Liyun Li, Tielin Liang, and Dongming Wang |
| 14:30-15:00 | Constraints for Continuous Reachability in the Verification of Hybrid Systems by Stefan Ratschan and Zhikun She |
| 15:00-15:30 | Using Hajós' Construction to Generate Hard Graph 3-Colorability Instances by Sheng Liu and Jian Zhang |
| 15:30-16:00 | Tea Break |
| Chair: Shilong Ma | 16:00-16:30 | Finding Relations Among Linear Constraints by Jun Yan, Jian Zhang, and Zhongxing Xu |
| 16:30-17:00 | Labeled @-Calculus: Formalism for Time-Concerned Human Factors by Tetsuya Mizutani, Shigeru Igarashi, Yasuwo Ikeda, and Masayuki Shio |
| 17:00-17:30 | Enhanced Theorem Reuse by Partial Theory Inclusions by Immanuel Normann |
| 18:00- | Reception Dinner |
| Chair: William McCune | |
| 09:00-10:00 | Invited Talk: Mechanization of Mental Labor and Mechanization of Mathematics by Wen-tsün Wu |
| 10:00-10:30 | Tea Break |
| Chair: David J. Jeffrey | 10:30-11:00 | Some Properties of Triangular Sets and Improvement upon Algorithm CharSer by Yong-Bin Li |
| 11:00-11:30 | A New Definition for Passivity and Its Relation to Coherence by Moritz Minzlaff and Jacques Calmet |
| 11:30-12:00 | A Full System of Invariants for Third-Order Linear Partial Differential Operators by Ekaterina Shemyakova |
| 12:00-14:00 | Lunch |
| Chair: Thérèse Hardin | 14:00-15:00 | Invited Talk: Semantic Guidance for Saturation Provers by William McCune |
| 15:00-15:30 | Tea Break |
| Chair: Jian Zhang | 15:30-16:00 | Extension of First-Order Theories into Trees by Khalil Djelloul and Thi-Bich-Hanh Dao |
| 16:00-16:30 | The Confluence Problem for Flat TRSs by Ichiro Mitsuhashi, Michio Oyamaguchi, and Florent Jacquemard |
| 19:00- | Banquet |
| Chair: Heisuke Hironaka | 09:00-10:00 | Invited Talk: Interactive Mathematical Documents by Arjeh M. Cohen |
| 10:00-10:30 | Tea Break |
| Chair: Masahiko Sato | 10:30-11:00 | A Search Engine for Mathematical Formulae by Michael Kohlhase and Ioan Sucan |
| 11:00-11:30 | Hierarchical Representations with Signatures for Large Expression Management by Wenqin Zhou, Jacques Carette, David J. Jeffrey, and Michael Monagan |
| 12:00-14:00 | Lunch |
| Chair: Dongming Wang | 14:00-14:30 | An Algorithm for Computing the Complete Root Classification of a Parametric Polynomial by Songxin Liang and David J. Jeffrey |
| 14:30-15:00 | Quantifier Elimination for Quartics by Lu Yang and Bican Xia |
| 15:00-15:30 | On the Mixed Cayley-Sylvester Resultant Matrix by Weikun Sun and Hongbo Li |
| 15:30-16:00 | Tea Break |
| Chair: Aart Middeldorp | 16:00-16:30 | Implicitization of Rational Curves by Yongli Sun and Jianping Yu |
| 16:30-17:00 | Operator Calculus Approach to Solving Analytic Systems by Philip Feinsilver and René Schott |
| 17:00-17:10 | Closing |