HOL4相关论文
有限域乘法是数据编码、解码及数据加密算法中的核心运算。为了保证算法正确地完成编解码和加密的功能,必须对有限域乘法电路设计......
机器人是综合了机械、电子、计算机、传感器、控制技术、人工智能、仿生学等多种学科的复杂智能机械,目前已成为世界各国的研究热......
机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的......
积分是许多数学理论的基础，如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广，应用更加方便。将G......
定理证明是一种形式化方法，在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础，实数二项式系数是分......
连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算......
回 回 产卜爹仇贱回——回 日E回。”。回祖 一回“。回干 肉果幻中 N_。NH lP7-ewwe--一”＄ MN。W;- __._——————》 砧叫]们......
为了增强基于遗传算法的水下群机器人路径规划算法正确性的说服力，使用定理证明对其进行形式化研究，给出算法在定理证明器HOL4中的形......
针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一......
随着微电子技术的高速发展，软硬件系统设计的复杂度飞速增长，苛刻应用环境对系统的可靠性要求不断提高，这些都对系统设计的正确性验证......
