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

该项目为国家自然科学基金资助面上项目（项目批准号：61571064）。

该项目研究基于证明辅助工具 Coq 和多项式代数方法的智能信号处理问题。提出的预期目标为：

建立一个基于证明辅助工具 Coq 的信息系统理论的机械化计算机平台环境。充分利用该平台强大的归纳构造演算功能，对信息系统理论中的一些基本理论给出形式化、机械化证明的构架与尝试。

在此基础上，融合数学机械化理论中基于符号数值混合计算的多项式代数方法。充分发挥 Coq 人机交互、形式化归纳构造演算功能和多项式代数方法的自动化、精确和完备的特点，实现证明辅助工具 Coq 与多项式代数方法的结合。

进而，对信息系统理论中的若干公开难题进行有益的探索，尝试在一定程度的解答，并考虑该平台在信息科学中的相关应用。

对基于证明辅助工具 Coq 和多项式代数方法的智能信号处理进行了深入的理论分析。在数学机械化及定理机器证明方面有所突破，完成了相应的程序设计。在成果应用与推广方面有所贡献。

该项目为国家自然科学基金资助面上项目（项目批准号：61571064）。

该项目研究基于证明辅助工具 Coq 和多项式代数方法的智能信号处理问题，提出的预期目标为：建立一个基于证明辅助工具 Coq 信息系统理论的机械化计算机平台环境，充分利用该平台强大的归纳构造演算功能，对信息系统理论中的一些基本理论给出形式化、机械化证明的构架与尝试。在此基础上融合数学机械化理论中基于符号数值混合计算的多项式代数方法，充分发挥 Coq 人机交互、形式化归纳构造演算功能和多项式代数方法的自动化、精确和完备的特点，实现证明辅助工具 Coq 与多项式代数方法的结合。进而对信息系统理论中的若干公开难题进行有益的探索，尝试在一定程度的解答，并考虑该平台在信息科学中的相关应用。

对基于证明辅助工具 Coq 和多项式代数方法的智能信号处理进行了深入的理论分析，在数学机械化及定理机器证明方面有所突破，完成了相应的程序设计，在成果应用与推广方面有所贡献。