声明
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。
国内刊号：11-1777/TP
国际刊号：1000-1239
发布日期:
作者：石海鹤,蓝孙文,刘日明,石海鹏,王岚,钟林辉,
关键词：序列比对, PAR方法, 形式构造, Isabelle定理证明器,
序列比对是生物序列分析中的一个经典问题，旨在找出序列之间的相似性，它对于发现生物序列中的功能、结构和进化信息都具有重要的意义.该问题可分为双序列比对和多序列比对2类，现有工作多针对特定算法展开，没有设计通用的求解方法；此外，甚少涉及算法可信性的研究.从生物序列比对问题的形式化规约出发，通过深入分析问题的性质，刻画问题求解的本质特征，借助形式化方法PAR（partitionandrecursion）设计了序列比对动态规划算法的统一构造框架seqAlign；展示了应用该框架构造序列数为3的多序列比对算法的过程，并使用Isabelle定理证明器对构造结果进行形式化验证；利用PAR平台生成了该算法的C++可执行程序，进一步分析了由seqAlign框架机械化构造其他类型序列比对算法的过程.通过严密的规约精化和形式验证，有效地保证了生成算法的可信性；开发的seqAlign框架提供了序列比对问题类的通用求解方案，显著提高了序列比对算法族生成的效率.研究结果在生物序列分析中序列比对问题上的成功应用，从方法学和实践上可为复杂生物信息学领域高可靠算法的构造提供参考.
来源：2025年第1期
《计算机研究与发展》期刊编辑部
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。