图搜索问题算法推导及形式化证明

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.     

二叉树排序非递归算法推导及形式化证明

非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.     

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.     

形式化开发若干组合数学问题的算法

计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最终可得到简洁、易理解、可靠性高的算法程序.对形式化方法开发组合算法做了积极的探索,有利于促进组合算法设计自动化的研究及形式化开发方法的推广应用.     

局间通信负荷监控问题的形式化方法

利用最新时段演算等理论，形式化负荷监测功能的告警原理和组合输出问题，并进行必要的形式化推导，以确保规范说明具有可理解性和准确性．还给出了实现监控的核心算法．     

二叉树队列关系问题非递归算法的推导及形式化证明

该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类问题是基于2个母算法的功能加以实现的,由此派生出3类问题.首先,对这3类派生问题进行推导,得到递...     

一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法

形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一,尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作,以自定义泛型抽象顺序设计语言Apla为基础,进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言,使其既支持顺序算法的验证又能有效地验证并发分布式算法.在依赖-卫式推理的基础上,提出一种新颖的2层并发分布式算法形式化验证方法,其中系统层用于处理并发级验证,而组件层用于处理顺序级验证.最后,通过2个实例验证了该方法的有效性和可行性.     

John圆盘的判定

复分析是基础数学的一个研究方向,在复平面上共形映射的条件下研究John圆盘的特点,针对Jonh圆盘的几何定义,推导出一个具有充要条件性质的判定,通过推导过程中的放缩变换限定出M和δ的与c有关的估值．     

3个变形背包问题的形式化推导

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用.     

复杂算法程序的规范证明和形式推导

能否实现复杂算法程序的规范证明和形式推导是检验某种形式化方法有无生命力的重要标志。本文介绍了这一领域的研究现状,重点综述了作者近年来提出的复杂算法程序形式化技术,以典型实例说明了使用这些技术的方法。     

带量词的合一算法

Ｒｏｂｉｎｓｏｎ于 １９６５年提出了归结原理，其主要工作是 Ｕｎｉｆｉｃａｔｉｏｎ算法。这个算法只能处理不带量词的子句公式，它不能用来发现定理的自然演绎证明。本文的算法能处理量词，它能用在基于自然演绎的定理证明系统上。文中给出合一定理的证明，基于此算法的自动自然演绎系统已实现，用它证明了Ａｎｄｒｅｗｓ；Ｂｌｅｄｓｏｅ和Ｐｅｌｌｏｔｉｅｒ挑战性问题。     

A Worsted Yarn Virtual Production System Based on BP Neural Network

Back-Propagation (BP) neural network and its modified algorlthm are introduced. Two series of BP neural network models have been established to predict yarn properties and to deduce wool fiber qua/ides. The results from these two series of models have been compared with the measured values respectively, proving that the accuracy in both the prediction model and the deduction model is high. The experimental results and the corresponding analysis show that the BP neural network is an efficient technique for the quality prediction and has wide prospect in the application of worsted yam production system.     

AC-3编码器中的高效比特分配算法

基于对信噪比偏移量的定量分析,得出待分配比特数与信噪比偏移量之间的理论估算公式,从而能够有效逼近信噪比偏移量的最佳值．在此基础上提出了一种基于一次逼近和收敛控制的高效比特分配算法,分别以迭代次数和剩余比特2个参数来衡量比特分配的效率和精度．实验结果表明,该算法所需的平均搜索次数约为传统算法的71．4％,使得AC-3编码器比特分配的精度和效率均有明显提升．     

加入动量项的改进盲分离算法

在盲信号分离算法的推导过程中,常采用最速下降法、自然梯度和牛顿法等对代价函数进行最小化,推导过程复杂．文中仿照在BP神经网络算法中加入动量项使算法得到改进这一方法,提出在互累积量迫零算法的推导中加入动量项．加入动量项的改进算法尽可能地保持了输出分量之间的独立,并在保持和原算法一样简单迭代的前提下,提高了收敛速度,且使训练避免陷入局部极小．仿真结果表明该算法的分离误差减小,能有效分离源信号．     

命题公式的一种演绎判定方法

命题公式的判定是人工智能领域中的一个核心问题。目前命题公式的判定方法大都是基于语义的,不能给出演绎过程,而这种演绎过程是许多推理性应用的重要依据,本文针对命题演算系统L,给出了一种可同时给出演绎过程的判定方法——演绎判定方法。首先提出了消解复杂性的两种范式：最简范式和文字范式,在此基础上给出了L的可判性定理的演绎证明及命题公式的演绎判定算法P(F),并基于ML语言设计了基于P(F)的演绎判定机DMBD。     

数字电视信道传输中RS译码算法的研究

针对数字电视译码电路复杂,译码速度不高的缺点,利用多项式带余除法的相关推论,提出一种改进型欧几里德算法．与传统欧几里德算法相比,该算法在求解关键方程的过程中能够较为容易地得到错误值多项式和错误位置多项式,从而可以降低硬件电路的复杂性,提高译码速度．仿真结果表明当误码个数不超过错误容限时,该算法能够完成正确译码的效果．     

一种新型谐波检测算法的MATLAB仿真

在对负载电流分析的基础上,引出了基于最小补偿电流的畸变电流检测算法。通过理论分析和严密的数学推导,证明了该算法的正确性和可行性。最后基于MATLAB仿真平台对该算法进行仿真,仿真结果表明该算法具有较高的检测精度。     

基于服务质量的Web服务优化选择算法及仿真

提出一种基于服务非功能属性的Web服务优化选择的多目标遗传算法.考虑到在服务选择时组合方案中的控制结构、具体服务之间的关联性和多个服务质量指标之间的折衷这三方面的约束,对服务选择建立分层模型给出优化选择的形式化定义.在此基础上,采用多目标遗传算法求解优化服务选择.首先设计了适合的染色体编码方式,以表示可行的服务选择方案...     

闭环增益成形算法的模型摄动

为了给出闭环增益成形算法的模型摄动形式,用小增益理论和H混合灵敏度算法的结果进行推导,发现闭环增益成形算法的模型摄动形式与灵敏度函数的形式相同,该结论对用闭环增益成形算法设计鲁棒控制器时系统所能忍受的模型摄动大小的确定具有指导意义．闭环增益成形算法的优点是设计过程简单,物理意义明显．     

数据分类的两步矩阵投影算法

化工过程的数据分类是进行数据校正和协调计算的基础。常用的两层次矩阵投影变换算法在对未测数据进行分类时,可能无法识别出所有的不可估计型数据。为了准确地将可估计型和不可估计型数据分开,采用Crowe等人提出的投影矩阵,引入矩阵的绝对线性无关列的概念,提出了新的数据分类方法。数学推导证明,此方法对化工过程未测数据分类彻底,并用一个示例将新旧算法对未测数据的分类结果进行了对比,验证了新算法作数据分类的正确性。