《基於證明輔助工具Coq和多項式代數方法的智慧型信號處理》是依託北京郵電大學，由郁文生擔任項目負責人的面上項目。
基本介紹
- 中文名：基於證明輔助工具Coq和多項式代數方法的智慧型信號處理
- 項目類別：面上項目
- 項目負責人：郁文生
- 依託單位：北京郵電大學
項目摘要,結題摘要,
項目摘要
結合證明輔助工具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項。研究者成員獲得包括吳文俊人工智慧自然科學獎在內的多項獎勵。
