一种基于Coq的拉普拉斯变换形式化验证方法

摘要

本发明公开了一种基于定理证明器Coq的拉普拉斯变换形式化验证方法，通过在定理证明器Coq中对拉普拉斯变换进行形式化定义并且验证了拉普拉斯变换的主要性质。本发明利用定理证明器Coq严谨性和可靠性解决了传统方法不能精确验证拉普拉斯变换的弊端。主要包括以下步骤：(1)拉普拉斯变换定义的形式化：在定理证明器Coq中采用微分、积分、极限、复数和复变函数等理论实现定义的形式化；(2)拉普拉斯变换存在性定理的形式化：对拉普拉斯变换的存在定理进行形式化描述；(3)拉普拉斯变换基本性质的形式化证明：在Coq定理证明器中对拉普拉斯变换的线性性质、频移性质、微分性质和积分性质进行形式化证明。