1706
郁文生教授，北京邮电大学，电子工程学院。在系统鲁棒控制理论、时滞系统稳定性分析、线性系统同时镇定、定理机器证明等方面做出一系列创新性成果，在《中国科学》、《科学通报》、《IEEE Trans.》系列等国内外重要学术刊物发表论文七十余篇，多篇被SCI、EI、ISTP三大权威检索机构收录。郁文生教授在智能科学与信息科学相关领域进行了长期深入研究。
专家简介
郁文生教授，北京邮电大学，电子工程学院。在系统鲁棒控制理论、时滞系统稳定性分析、线性系统同时镇定、定理机器证明等方面做出一系列创新性成果，在《中国科学》、《科学通报》、《IEEE Trans.》系列等国内外重要学术刊物发表论文七十余篇，多篇被SCI、EI、ISTP三大权威检索机构收录。2017年，获得“中国智能科学技术最高奖”——吴文俊人工智能自然科学奖二等奖。郁文生教授在智能科学与信息科学相关领域进行了长期深入研究，主要工作为：
(1)将数学机械化的理念和思想应用于信息科学的研究，在系统鲁棒控制、时滞系统稳定性分析及线性系统同时镇定等方面做出一系列创新性成果:其中包括给出了传递函数基于矩阵不等式的正实性条件;对四次区间多项式族鲁棒严格正实综合问题给出正面肯定的回答;利用多项式完全判别系统给出多项式严格正实域的完整刻画并解决了鲁棒严格正实综合问题，给出时滞系统全时滞稳定的代数判据;利用复分析理论，完整解决线性系统同时镇定中著名的广义香槟问题;
(2)在基于Coq的数学定理证明系统方面，自 2015年以来，其研究团队已初步开发了“公理化集合论”和“近世代数基础”两个定理机器证明系统，“点集拓扑基础”系统也已初步搭建。对布尔巴基数学学派特别强调的现代数学三大母结构——序结构、代数结构、拓扑结构——的机器证明系统实现进行了有意义的探索尝试。
项目简介
本项目为数学机械化与人工智能，主要研究工作包括以下5个方面:
系统鲁棒严格正实综合：传递函数的鲁棒严格正实综合，本质上可化为一些非线性代数方程组或不等式组的求解问题。通过讨论不同文献中对严格正实性的不同定义之间的区别与联系，借助新近发展的多项式完全判别系统，给出系数空间中传递函数鲁棒严格正实域的完整刻画，研究鲁棒严格正实域的对综合问题有意义的特有性质，并结合凸规划的有关方法，由此提出一种新的切实可行的鲁棒严格正实综合设计方法。
时滞系统全时滞稳定的代数判据：时滞微分系统全时滞稳定性的研究在理论和应用上都有重要的意义。特别地，从控制理论的角度看，系统全时滞稳定即表明该系统对于时滞具有很好的鲁棒性和可靠性。我们首先讨论了一类形式较为一般的任意维线性多时滞滞后型微分系统的全时滞稳定性问题。利用多项式完全判别系统，给出该系统全时滞稳定的代数判别准则。将多项式完全判别系统应用于中立型时滞微分系统全时滞稳定的判定，得到了中立型时滞微分系统便于应用的代数判据;当系统非全时滞稳定时，可进一步得到使系统稳定的时滞界限。
线性系统的同时镇定问题：线性系统的同时镇定问题是系统与控制理论中的基本问题，有着重要的理论意义和广泛的应用价值。为说明三个对象同时镇定问题的复杂性，Blondel等人在其研究过程中提出了法国香槟问题与比利时巧克力问题。申请者针对以上公开问题，进行了细致深入的研究，取得了显著成果：1、完全解答法国香槟问题及广义香槟问题。2、比利时巧克力系统的低阶控制器镇定。
正系统理论与应用：正系统是指在任何时刻系统的输入、状态和输出均为非负的动态系统。在正系统理论中，正实现问题是一个最为活跃的研究课题。我们对正实现的最小维数问题进行研究，取得了一系列的成果分为四个方面：1、首次讨论具有复极点的三阶离散时不变线性单输入单输出系统的最小正实现。2、针对具负极点的离散时不变线性单输入单输出系统的n阶有理传递函数，采用构造性方法，给出其存在n阶正实现的充分必要条件。3、结合非负逆特征值问题的研究，给出具有复极点的n阶离散时不变线性单输入单输出系统存在等阶正实现的条件。4、分别针对连续时间和离散时间的具有界时滞的正系统，给出系统渐近稳定的充分必要条件。
Coq系统与机器证明：机器证明是人工智能领域的重要研究方向之一，同时也是数学机械化研究的一项重要内容。自20世纪70年代以来，以吴文俊院士为核心的研究人员在机器证明和自动推理领域取得了一系列具有重大意义的研究成果。近年来数学定理的形式化证明的研究，随着计算机科学的迅猛发展、特别是交互式定理证明辅助工具Coq的出现，取得了长足的进展。我们建立了一个基于Coq的数学定理证明系统，充分利用强大的归纳构造演算功能，对信息系统理论中的一些基本理论给出形式化、机械化证明的构架与尝试。对布尔巴基数学学派特别强调的现代数学三大母结构——序结构、代数结构、拓扑结构——的机器证明系统实现进行了有意义的探索尝试。
实验室简介
郁文生教授所在北京邮电大学电子工程学院，具有优秀的科研队伍，能提供相关研究领域的权威数据库IEEE及Elsevier等的最新研究论文。所在智能信息实验室，能为本课题提供充分的软硬件支持。所在研究团队结构合理，富有团队协作精神。
项目组骨干成员, 项目其他成员均为北京邮电大学在读的博士生或硕士生, 其中大多数人曾参加过国家自然科学基金项目，并都有相关学术论文在国际刊物或国际会议发表，在相关领域内有很好的积累，这也使我们的研究团队充满活力。相信各成员能在本项目中发挥优势。
机器证明是北京邮电大学极具特色的研究领域，本项目依托北京邮电大学电子工程学院和计算机学院，具有良好的科研环境和科研条件，申请人与国内外同行的有着广泛接触及学术交流，能随时了解和掌握国际当前研究的最新方向及研究动态。申请人与中国科学院数学与系统科学研究院、自动化研究所、成都科分院、重庆绿色智能技术研究院，以及北京大学、清华大学、北京航空航天大学、中国矿业大学(北京)及上海大学等国内著名科研院所和高校有着良好的合作关系，这些单位的大型集群计算平台可以本项目中的“计算、测试与验证”环节中发挥作用。
