姓 名：杨 路

办公室：理科大楼A1703
电子邮件： lyang@sei.ecnu.edu.cn

教育背景
北京大学数学系毕业

研究兴趣
定理机器证明、符号计算、计算机自动推理、人工智能

工作经历
1979 — 1985 中国科技大学数学系 讲师、副教授。
1986 — 1991 中国科学院成都数理科学研究室 研究员、副主任。
1992 — 中国科学院成都计算机应用研究所 研究员。
1992 — 1996 中科院成都计算机所 数学与计算机科学研究中心 主任。
1992 — 1996 国家85攀登项目“机器证明及其应用” 专家委员会成员。
1993 年 任国际数学奥林匹克（IMO）中国国家代表队 领队、主教练。
1995 — 广州市数学与人工智能中心主任、广州大学软件所 教授（兼）。
1996 — 2003 北京大学数学科学学院 信息科学系 教授、系主任（兼）。
1997 — 1998 国家95攀登项目“数学机械化的研究与应用” 首席科学家。
1988 — 1989 澳大利亚国立大学等四所大学 客座教授。
1990 — 1991 意大利理论物理中心、德国Bielefeld大学等 客座教授。
1993 — 1994 美国纽约州立大学、Wichita州立大学等 客座教授。
1995年11月 访问联合国大学国际软件所。
1995年12月 访问新加坡国立大学。
1996年7月 访问奥地利符号计算研究所。
1997年9月 访问台北中中央研究院、台北清华大学等多个单位。
1998年3—7月 法国国家科研中心 客座研究员。 任研究员、计算机软件与理论博士生导师、数学博士生导师，培 养博士研究生13人、硕士研究生50多人。

荣誉和奖项
中国科学院“不等式机器证明与机器发现”知识创新项目首席科学家
国家973项目“数学机械化与自动推理平台”专家委员会成员
国家973课题“构造性实代数几何与不等式自动推理”主持人
1995年获中国科学院自然科学一等奖。
1997年获国家自然科学二等奖。
2001年获中国第8届专利博览会金奖。
2003年获全国“五一”劳动奖章。

主要论著
[1]Yang L, Distance coordinate used in geometric constraint solving, Lecture Notes in Artificial Intelligence 2930, pp. 216-229, Springer-Verlag, 2004.
[2]Yang L, Xia B, Automated Deduction in Real Geometry, Geometry Computation, pp. 248-298, World Scientific. 2004.
[3]杨 路，夏时洪，一类构造性几何不等式的机器证明，计算机学报，26(7): 769-778. 2003.
[4]杨 路，夏壁灿，计算实代数几何，符号计算选讲（王东明主编，杨 路等编著），pp.100-149, 清华大学出版社，2003年8月。
[5]夏壁灿，杨 路，多项式判别矩阵的若干性质及其应用，应用数学学报，26(4): 652-663. 2003
[6]Yang L, Zhang J & Zhang W, On number of circles intersected by a line,J. of Combinatorial Th.Ser. A, 98 (2002), 2: 395-405.
[7]Xia B C & Yang L, An algorithm for isolating the real solutions of semi-algebraic systems and its applications,J. Symbolic Computation，34 (2002), 461-477.
[8]Yang L & Zhang J, A practical program of automated proving for a class of geometric inequalities, Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence 2061, pp.41-57, Springer-Verlag, 2001.
[9]Yang L, Automatically solving semi-algebraic systems, Proceedings of ATCM 2001, ATCM, Inc., 2001. (大会特邀报告)
[10]杨 路，侯晓荣，夏壁灿，自动发现不等式型定理的一个完备算法，中国科学E 辑，2001年第3期。