基于证明辅助工具Coq和多项式代数方法的智能信号处理

Using the polynomial algebra method based on mixed symbolic-numerical computation, combining with the proof assistant tool Coq, the frame and the implementations of the automated proving for some fundamental problems in basic information theory will be formulated systematically. We also try to solve some famous open problems in information science. In 2005, using the computer proof assistant tool Coq, the well-known "four color theorem" was proved by two world famous computer scientists Gonthier and Werner. Recently, the first 2140 zeros of the Riemann zeta function, whose absolute values of imaginary parts are less than 1501, have been successfully verified by using the Maple calculation functions. We can also present the exact values of these zeros, accurate to over 14 decimal places. 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 70 academic journal 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. Power Electronics> , one paper in <IEEE Trans. Intell. Transp. Syst.> and five papers in <IEEE Trans. Circuits. Syst.>.

结合证明辅助工具Coq和基于符号数值混合计算的多项式代数方法，系统化地给出一批信息基础理论中基本命题的机器自动证明构架和实现，并尝试一些著名公开难题的解答。2005年，国际计算机专家Gonthier and Werner成功基于Coq给出了著名的“四色定理”的计算机证明，我们最近基于Maple的数值计算功能也成功验算了Riemann蔡塔函数(zeta funcition)虚部绝对值小于1501的2140个零点，并且可以具体给出这些零点的值，精度已达小数点后第14位。机器证明得出的结论有时可能是已知结果的推广，其方法本身对同类学科有示范性。将提供更多的例子表明算法和软件的有效性。申请人已在上述几个方面进行了部分有益的探索，均得到令人满意的结果，有较强的研究基础。申请人已发表期刊论文七十余篇，其中《IEEE Trans.》系列八篇，《中国科学(中英文)》八篇。

结合证明辅助工具Coq和基于符号数值混合计算的多项式代数方法，系统化地给出一批信息基础理论中基本命题的机器自动证明构架和实现，并尝试一些著名公开难题的解答。2005年，国际计算机专家Gonthier and Werner成功基于Coq给出了著名的“四色定理”的计算机证明，我们最近基于Maple的数值计算功能也成功验算了Riemann蔡塔函数(zeta funcition)虚部绝对值小于1501的2140个零点，并且可以具体给出这些零点的值，精度已达小数点后第14位。机器证明得出的结论有时可能是已知结果的推广，其方法本身对同类学科有示范性。将提供更多的例子表明算法和软件的有效性。申请人已在上述几个方面进行了部分有益的探索，均得到令人满意的结果。期间发表期刊和会议论文 26 篇，期刊论文发表于《IEEETrans. PE》、《Journal of Systems Science and Complexity》等。科学出版社出版专著，受“华罗庚-吴文俊”基金资助，并收录于数学机械化丛书，获国家软件著作权4项。研究者成员获得包括吴文俊人工智能自然科学奖在内的多项奖励。