信息科学中若干理论问题的机械化证明

Based on the recent development in automated inequality-type theorem proving, such as the complete algorithm for automated discovering of inequality-type theorems and the successive difference substitution method, the frame and the implementations of the automated proving for some fundamental problems in system theory will be formulated. These fundamental problems include Kharitonov theorem, determined conditions for controllability or observability in linear systems, pole assignment of linear systems, qualitative analysis of ordinary differential equations(ODEs), safety verification for hybrid systems, and Hurwitz stability theorem et al. The conclusions obtained from automated proving sometimes may extend the known results; and the method would be of exemplariness to analogous types of theorems. The effectiveness of the algorithm and package will be illustrated by some more examples. The applicant obtained some valuable results in the previous research and published about sixty reserch papers, including eight papers in <Science in China>(Chinese version and English version), one paper in <IEEE Trans. Autom. Control> , one paper in <IEEE Trans. Intell. Transp. Syst.> and five papers in <IEEE Trans. Circuits. Syst.>.

利用新近发展的自动发现不等式型定理的完备算法及差分代换算法等机器证明方法，给出一批系统理论中的基本命题的机器自动证明构架和实现。这些基本命题包括哈里托诺夫（Kharitonov）定理、线性系统的可控可观性判定条件、线性系统的极点配置条件、常微分方程的定性分析、混成系统的安全性检验、Hurwitz稳定性判定定理等。机器证明得出的结论有时可能是已知结果的推广；其方法本身对同类命题有示范性。将提供更多的例子表明算法和软件的有效性。申请人已在上述几个方面进行了部分有益的探索，均得到令人满意的结果，有较强的研究基础。申请人已发表期刊论文六十余篇，其中《IEEE Trans.AC》、《IEEE Trans.ITS》及《IEEE Trans.CAS》七篇，《中国科学（中英文）》八篇。

利用新近发展的自动发现不等式型定理的完备算法及差分代换算法等机器证明方法，给出一批系统理论中的基本命题的机器自动证明构架和实现。这些基本命题包括哈里托诺夫（Kharitonov）定理、线性系统的可控可观性判定条件、线性系统的极点配置条件、常微分方程的定性分析、混成系统的安全性检验、 Hurwitz 稳定性判定定理等。机器证明得出的结论有时可能是已知结果的推广；其方法本身对同类命题有示范性。将提供更多的例子表明算法和软件的有效性。申请人已在上述几个方面进行了部分有益的探索，均得到令人满意的结果。期间发表期刊和会议论文 30 篇，期刊论文发表于《IEEE Trans. PE》、《Journal of Systems Science and Complexity》、《电机与控制学》、《计算机科学》及《电力系统自动化》等，获软件著作权一项，研究者成员获得包括吴文俊人工智能自然科学奖在内的多项奖励。