● 摘要
作为数学机械化思想的代表性成果之一，自动定理证明器至今不仅实现了许多数学定理的机械化证明，而且越来越多的实际应用问题也在其独特优势下得到了解决。非线性科学研究是目前的前沿热点研究领域，海洋中内孤立波的传播模型就是非常具有代表性的非线性模型。目前学者们解出了许多的传播模型解析解，却没有对应的解析解正确性验证过程出现，究其原因则是验证的复杂性以及产生的状态空间爆炸问题。微分动态逻辑是以微分方程为对象以验证复杂混成系统性质的逻辑，它并不涉及求解过程而是使用逻辑归纳的方法验证形式化对象。本文将模型解析解的验证过程形式化为微分动态逻辑语句，成功地验证了其正确性。另一方面，论文中提出增强的二维模态分解算法用于处理真实海洋SAR图并反演出了部分内孤立波传播参数。同时，在适用于相同海域的内孤立波传播模型下结合实测数据也得到其传播参数，与上述反演得到的参数进行对比，在理论与实践相结合中验证模型解析解的正确性。本文的主要成果有以下几个方面：1. 根据海洋SAR图的实际特征，提出了增强的二维模态分解算法，消除了斑点噪声对SAR图分解带来的影响，较大地提升了海洋SAR图的多尺度分离效果。并且根据分解结果图像以及内孤立波传播参数反演理论反演出真实SAR图对应的内孤立波传播参数。2. 给出适用于中国南海海域的内孤立波传播模型方程及其解析解，结合反演得到的波群速度参数推导出理论模型下对应的其他内孤立波传播参数，将其与真实SAR图对应的内孤立波传播实测数据进行对比，不但保证了增强二维模态分解算法的实用性和可行性，更重要的是验证了内孤立波传播模型方程解析解的正确性。3. 给出了微分动态逻辑的语法和语义定义。根据微分不变量的技术在KeYmaera自动定理证明器中形式化了解析解的验证过程并且验证过程执行成功。解决了普通验证过程状态空间爆炸的难题，最终首次成功地将微分动态逻辑用于非线性方程解析解的验证。针对一个较简单的偏微分方程实现了上述过程，并且根据微分不变量理论手工推导得到相应结果，与所给出的形式化代码一致，保证了形式化过程的正确性。