期刊文献+
共找到18篇文章
< 1 >
每页显示 20 50 100
基于概率逻辑推理的高阶互补云API推荐方法 被引量:2
1
作者 陈真 谢登辉 +3 位作者 王小龙 孙梦梦 刘啸威 申利民 《计算机学报》 EI CAS CSCD 北大核心 2024年第8期1922-1948,共27页
云时代,云API作为服务交付、数据交换和能力复制的最佳载体,已成长为当今面向服务软件开发和企业数字化转型不可或缺的核心要素.然而动态开放网络中持续增长的云API在给开发者提供了更多选择的同时,也将其淹没在海量的云API选择之中,设... 云时代,云API作为服务交付、数据交换和能力复制的最佳载体,已成长为当今面向服务软件开发和企业数字化转型不可或缺的核心要素.然而动态开放网络中持续增长的云API在给开发者提供了更多选择的同时,也将其淹没在海量的云API选择之中,设计有效的云API推荐方法就此成为API经济健康发展中迫切要解决的现实问题.但是,现有研究主要利用搜索关键词、服务质量和调用偏好进行建模,生成质量高功能单一的云API推荐列表,没有考虑服务化软件实际开发中开发者对多元化高阶互补云API的客观需要.高阶互补云API推荐旨在为多个查询云API生成多元互补云API列表,要求推荐结果与查询云API均互补,以满足开发者的联合需求.针对此问题,本文提出基于概率逻辑推理的高阶互补云API推荐方法(Probabilistic Logic Reasoning for High-order Complementary Cloud API Recom⁃mendation,PLR4HCCR).首先,通过云API生态真实数据分析论证云API互补推荐需求的必要性和互补关系建模中替补噪声的客观存在,为云API互补推荐问题研究提供动机和数据支持.其次,采用Beta概率嵌入对云API及其之间的关系约束进行编码,以刻画云API间互补关系的不确定性和支持互补逻辑推理.接着,设计由投影、取反和交并三个基本逻辑算子构建的互补关系逻辑推理网络,使查询集中的每个云API获得非对称互补关系感知和替补噪声消解约束下的互补云API表示.然后,引入注意力机制为查询云API的互补云API分配不同权重,增强高阶互补云API基向量的表征能力.在此基础上,采用KL散度度量高阶互补云API基向量与候选云API之间的距离,并根据KL散度排序生成高阶互补性可感知下的云API推荐结果.最后,我们利用两个真实云API数据集在不同阶互补推荐场景下进行实验,实验表明,与传统启发式推荐方法和深度学习推荐方法相比,PLR4HCCR在互补关系感知推理和替补噪声消解方面均具有较大的优势,继而使其在低阶、高阶和混合阶互补云API推荐中均展示出更优的推荐效果和更强的泛化能力.进一步,超参数敏感性实验、实例分析和用户调查验证了方法的有效性、实用性和可行性,这使结合高阶互补关系的云API推荐方法PLR4HCCR不仅更有可能生成开发者满意的结果,而且可有效提升云API服务提供者的收益. 展开更多
关键词 面向服务软件开发 云API推荐 高阶互补 逻辑推理 Beta概率嵌入
在线阅读 下载PDF
REACHABILITY/CONTROLLABILITY OF HIGH ORDER MIX-VALUED LOGICAL NETWORKS 被引量:4
2
作者 LIU Zhenbin WANG Yuzhen 《Journal of Systems Science & Complexity》 SCIE EI CSCD 2013年第3期341-349,共9页
This paper addresses the teachability/controllability of high order mix-valued logical control networks by using the semi-tensor product method, and presents some necessary and sufficient conditions for the reachabili... This paper addresses the teachability/controllability of high order mix-valued logical control networks by using the semi-tensor product method, and presents some necessary and sufficient conditions for the reachability/controllability. The high order mix-valued logical network is converted into an algebraic form first, baaed on which the reachability/controllability of the system is then investigated, and several necessary and sufficient conditions are established. The study of several illustrative examples shows that our new method is very effective in dealing with the reachability/controllability of high order mix-valued logical control networks. 展开更多
关键词 CONTROLLABILITY high order mix-valued logical control network REACHABILITY semi-tensor product.
原文传递
High-Order Two-Dimension Cluster Competitive Activation Mechanisms Used for Performing Symbolic Logic Algorithms of Problem Solving
3
作者 帅典勋 《Journal of Computer Science & Technology》 SCIE EI CSCD 1995年第2期124-133,共10页
This paper presents a neural network approach, based on high-order two-dimension temporal and dynamically clustering competitive activation mecha-nisms, to implement parallel searching algorithm and many other symboli... This paper presents a neural network approach, based on high-order two-dimension temporal and dynamically clustering competitive activation mecha-nisms, to implement parallel searching algorithm and many other symbolic logicalgorithms. This approach is superior in many respects to both the commonsequential algorithms of symbolic logic and the common neura.l network usedfor optimization problems. Simulations of problem solving examples prove theeffectiveness of the approach. 展开更多
关键词 high-order temporal network competitive activation symbolic logic algorithm dynamic clustering optimization problem
原文传递
运用定理证明的形式化方法验证SpaceWire编码电路 被引量:10
4
作者 李黎明 关永 +2 位作者 吴敏华 张杰 施智平 《小型微型计算机系统》 CSCD 北大核心 2012年第6期1372-1376,共5页
我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验... 我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验证,运用定理证明的形式化方法,在HOL4工具上对该电路的设计实现与规范要求的一致性进行验证,克服了传统验证方法的局限性. 展开更多
关键词 形式化验证 SpaceWire标准 DS编码 定理证明 高阶逻辑
在线阅读 下载PDF
两相邻路口交通信号的协调控制 被引量:36
5
作者 李灵犀 高海军 王飞跃 《自动化学报》 EI CSCD 北大核心 2003年第6期947-952,共6页
传统路口的控制算法大多研究单个路口的信号控制情况 .该文根据路口之间的相互关系 ,利用高阶广义神经网络及模糊推理提出了两个相邻交通路口的协调算法 .利用此算法设计的交通信号控制器 ,可以有效地协调两相邻路口的红绿灯信号 。
关键词 路口交通信号 协调控制 控制算法 模糊控制 神经网络 交通路口 模糊推理
在线阅读 下载PDF
重写对策在基于HOL的形式化证明中的应用 被引量:1
6
作者 张杰 毛丹雯 +1 位作者 关永 施智平 《计算机工程与设计》 CSCD 北大核心 2013年第10期3664-3668,共5页
讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用。通过REWRITE_TAC对策、ASM_REWRITE_TAC对策和RW_TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match... 讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用。通过REWRITE_TAC对策、ASM_REWRITE_TAC对策和RW_TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较。进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题。 展开更多
关键词 定理证明方法 高阶逻辑定理证明系统 形式化证明 目标制导法 重写对策
在线阅读 下载PDF
基于HOL4的形式化方法
7
作者 张杰 饶文博 +1 位作者 王少超 李晓娟 《计算机系统应用》 2016年第2期202-207,共6页
针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以... 针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质. 展开更多
关键词 定理证明 形式化方法 高阶逻辑 乘法器 HOL4 形式化建模
在线阅读 下载PDF
汇率的比价——杠杆属性系统、高阶逻辑问题与宏观混沌机制
8
作者 吴文 《复旦学报(社会科学版)》 CSSCI 北大核心 2017年第3期129-139,共11页
汇率是国际金融领域中的关键变量,在世界经济渐趋一体化的时代背景下,汇率同时成为影响一国经济运行内部状况的重要因素。汇率的高低对经济的内涵与外延增长有不同的影响,从而使经济的内部均衡呈现不同的状态。本文首先尝试在教育部重... 汇率是国际金融领域中的关键变量,在世界经济渐趋一体化的时代背景下,汇率同时成为影响一国经济运行内部状况的重要因素。汇率的高低对经济的内涵与外延增长有不同的影响,从而使经济的内部均衡呈现不同的状态。本文首先尝试在教育部重大课题攻关项目"人民币均衡汇率问题研究"中所建立的汇率决定的内部均衡模型的理论框架内对其进行修正;其次从汇率与经济增长的反身性关系角度对原模型框架进行了反思,并从中引申出高阶逻辑问题与宏观混沌机制;最后对该问题进行了哲学层面的探究,并从一个新的视角阐释了辩证法与形而上学的关系。 展开更多
关键词 汇率 经济增长 高阶逻辑 混沌
原文传递
实数二项式系数在HOL4中的形式化 被引量:1
9
作者 师丽坤 赵春娜 +3 位作者 关永 施智平 李晓娟 叶世伟 《计算机科学》 CSCD 北大核心 2014年第2期15-18,共4页
定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系... 定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。 展开更多
关键词 实数二项式系数 高阶逻辑 定理证明 HOL4 分数阶微积分
在线阅读 下载PDF
群机器人区域覆盖算法高阶逻辑建模与验证 被引量:1
10
作者 尹晓娜 王国辉 +3 位作者 施智平 关永 张倩颖 张景芝 《小型微型计算机系统》 CSCD 北大核心 2022年第3期475-482,共8页
区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用... 区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群机器人工作场景的高阶逻辑表达;完成了机器人移动概率和平均移动概率的建模与验证;最终验证了一定时间步长内群机器人在特定区域内的覆盖率的正确性.为实现多种复杂场景下群机器人区域覆盖算法的高阶逻辑定理证明形式化分析奠定基础. 展开更多
关键词 群机器人 区域覆盖 高阶逻辑 定理证明 形式化验证
在线阅读 下载PDF
实现并行搜索和符号逻辑算法的高阶二维时态-竞争激励神经网络方法
11
作者 帅典勋 《计算机学报》 EI CSCD 北大核心 1995年第3期181-189,共9页
本文提出并行搜索和规划算法,以及实现它们的高阶二维时态-竟争激励神经网络.这种网络还能实现基于传统符号逻辑的许多问题求解算法.本文的方法克服了通常的神经网络求解优化问题的缺陷.同时,也避免了符号逻辑算法的串行性及符号... 本文提出并行搜索和规划算法,以及实现它们的高阶二维时态-竟争激励神经网络.这种网络还能实现基于传统符号逻辑的许多问题求解算法.本文的方法克服了通常的神经网络求解优化问题的缺陷.同时,也避免了符号逻辑算法的串行性及符号逻辑Systolic结构复杂性等问题.给出了求解隐式图搜索、LCS问题、TSP问题及0-1背包问题的实例. 展开更多
关键词 并行搜索 符号逻辑 算法 神经网络
在线阅读 下载PDF
光电跟踪系统的模糊Ⅱ型控制技术研究 被引量:5
12
作者 秦树旺 毛耀 包启亮 《激光技术》 CAS CSCD 北大核心 2021年第2期147-154,共8页
为了解决高型控制方法在光电伺服跟踪系统应用中存在的稳态精度与超调量之间的矛盾,设计了一种由多种群遗传算法(MPGA)优化的模糊Ⅱ型控制方法。该方法在经典Ⅰ型双闭环反馈控制器的速度环之前并联一个积分环节,将系统型别增加到Ⅱ型,... 为了解决高型控制方法在光电伺服跟踪系统应用中存在的稳态精度与超调量之间的矛盾,设计了一种由多种群遗传算法(MPGA)优化的模糊Ⅱ型控制方法。该方法在经典Ⅰ型双闭环反馈控制器的速度环之前并联一个积分环节,将系统型别增加到Ⅱ型,以此加快反应速度、减小稳态误差;并引入模糊控制器(FLC),根据系统状态动态调节积分环节的增益,实现动态高型控制,既抑制系统震荡,又保证稳态精度;然后用MPGA优化FLC的输入输出比例因子,得到最优控制参量。对该控制系统进行了理论分析,并将各阶段优化系统进行了对比实验。结果表明,在相同实验条件下,采用MPGA优化的模糊Ⅱ型控制系统实现了对系统的动态高型控制,既能保证原系统的超调量不变,又能将稳态误差减小88.55%,明显提高了控制系统的稳态精度。该研究对优化光电伺服跟踪系统是有帮助的。 展开更多
关键词 激光技术 动态高型控制系统 模糊控制 遗传算法
在线阅读 下载PDF
DES芯片抵御高阶差分功耗分析攻击方法研究
13
作者 李海军 马光胜 刘晓晓 《Journal of Semiconductors》 EI CAS CSCD 北大核心 2008年第2期376-380,共5页
分析独特的屏蔽方法及改进方法的不足,提出了逻辑层和算法层相结合抵御高阶差分功耗分析攻击的新方法,并给出芯片半定制设计流程.芯片关键部分电路采用自定义功耗恒定逻辑单元实现,非关键部分电路采用CMOS逻辑以减少功耗和面积.整体电... 分析独特的屏蔽方法及改进方法的不足,提出了逻辑层和算法层相结合抵御高阶差分功耗分析攻击的新方法,并给出芯片半定制设计流程.芯片关键部分电路采用自定义功耗恒定逻辑单元实现,非关键部分电路采用CMOS逻辑以减少功耗和面积.整体电路采用独特的屏蔽方法自定义轮实现.结果表明芯片能够抵御高阶差分功耗分析攻击,运算速度与现有方法相当,而所需资源比现有方法少. 展开更多
关键词 高阶差分功耗分析 独特的屏蔽方法 DES 灵敏放大器型逻辑
在线阅读 下载PDF
逻辑函数高阶布尔e偏导数求解算法的实现
14
作者 罗文强 王伦耀 夏银水 《浙江大学学报(理学版)》 CAS CSCD 北大核心 2018年第4期420-426,共7页
针对已有方法在求解布尔e偏导数时只能解决小规模电路的问题,提出了一种基于逻辑函数不相交运算的大函数高阶布尔e偏导数的求解算法.该方法将逻辑函数转化为不相交乘积项的集合,用逻辑函数的不相交运算替代布尔e导数运算中的逻辑"... 针对已有方法在求解布尔e偏导数时只能解决小规模电路的问题,提出了一种基于逻辑函数不相交运算的大函数高阶布尔e偏导数的求解算法.该方法将逻辑函数转化为不相交乘积项的集合,用逻辑函数的不相交运算替代布尔e导数运算中的逻辑"与"运算;并将不包含待求导变量的乘积项拆分出来,不参与布尔e导数运算,以达到降低算法复杂度、提高算法速度的目的.提出的算法用C语言编程实现,并用MCNC测试电路进行了测试.实验结果显示,本算法能快速实现大函数高阶布尔e偏导数的求解,求解效率与参与不相交运算的乘积项数量有关,但对输入变量的数量不敏感. 展开更多
关键词 e导数 e偏导数 高阶 逻辑覆盖 逻辑不相交运算
在线阅读 下载PDF
PEMFC系统过氧比的自适应高阶滑模控制 被引量:6
15
作者 马冰心 王永富 《控制理论与应用》 EI CAS CSCD 北大核心 2020年第2期253-264,共12页
调节控制质子交换膜燃料电池(PEMFC)空气供给系统过氧比(OER)在理想范围可有效提高PEMFC系统输出净功率.为此,本文首先结合反馈控制理论将非线性PEMFC空气供给系统转化为标准形,并对系统内部动态进行了稳定性分析.然后基于PEMFC空气供... 调节控制质子交换膜燃料电池(PEMFC)空气供给系统过氧比(OER)在理想范围可有效提高PEMFC系统输出净功率.为此,本文首先结合反馈控制理论将非线性PEMFC空气供给系统转化为标准形,并对系统内部动态进行了稳定性分析.然后基于PEMFC空气供给系统系统扩展的状态空间,并提出一种新型的自适应高阶滑模方法.该控制器不需PEMFC空气供给系统模型和干扰/不确定向的界已知的条件,自适应模糊逻辑系统可在线逼近系统中未建模动态.并且通过在线自适应获得的控制增益可保证系统跟踪误差收敛到原点附近的邻域内.最后,结合Lyapunov理论验证了系统的收敛性与稳定性,通过仿真和硬件在环实验进一步验证了该控制器的自适应性与优越性. 展开更多
关键词 质子交换膜燃料电池 过氧比 高阶滑模控制器 自适应模糊系统 LYAPUNOV稳定性 硬件在环实验
在线阅读 下载PDF
EQ-代数上M-算子研究
16
作者 高晓莉 王军涛 程晓云 《咸阳师范学院学报》 2023年第4期4-10,共7页
EQ-代数是高阶模糊逻辑所对应的一类重要逻辑代数,将其作为模糊逻辑理论的主要研究领域,对推动人工智能的发展有重要意义。文中主要在EQ-代数上引入Multiplier算子(M-算子)、单M-算子、幂等M-算子等算子的概念,并研究其相关性质,得到了M... EQ-代数是高阶模糊逻辑所对应的一类重要逻辑代数,将其作为模糊逻辑理论的主要研究领域,对推动人工智能的发展有重要意义。文中主要在EQ-代数上引入Multiplier算子(M-算子)、单M-算子、幂等M-算子等算子的概念,并研究其相关性质,得到了M-算子的复合依然是M-算子,并给出了保序M-算子的等价刻画,证明了在n元好的EQ-代数上,至少可以定义n个互异的M-算子;其次,讨论了M-算子与一些特殊映射(闭包算子、同态映射、幂等映射、恒等映射)之间的关系,给出了M-算子是恒等映射的等价刻画;最后,研究了EQ-代数E上关于M-算子f的不动点集(即Fixf(E))的相关性质,得到在给定条件下,M-算子的不动点集可以构成EQ-代数。 展开更多
关键词 高阶模糊逻辑 EQ-代数 Multiplier算子 不动点集
在线阅读 下载PDF
Analysis of Gene Networks for Arabidopsis Flowering
17
作者 Yansen Su Dazhi Meng +1 位作者 Eryan Li Shudong Wang 《Tsinghua Science and Technology》 SCIE EI CAS 2012年第6期682-690,共9页
The flowering time of Arabidopsis is sensitive to climate variability, with lighting conditions being a major determinant of the flowering time. Long-days induce early flowering, while short-days induce late flowering... The flowering time of Arabidopsis is sensitive to climate variability, with lighting conditions being a major determinant of the flowering time. Long-days induce early flowering, while short-days induce late flowering or even no flowers. This study investigates the intrinsic mechanisms for Arabidopsis flowering in different lighting conditions using mutual information networks and logic networks. The structure parameters of the mutual information networks show that the average degree and the average core clearly distinguish these networks. A method is then given to find the key structural genes in the mutual information networks and the logic networks respectively. Ten genes are found to possibly promote flowering with three genes that may restrain flowering. The sensitivity of this method to find the genes that promote flowering is 80%, while the sensitivity of the method to find the genes that restrain flowering is 100%. 展开更多
关键词 flowering gene gene network high-order logic mutual information systems biology
原文传递
Program Constructionby Verifying Specification
18
作者 林洪 陈国良 《Journal of Computer Science & Technology》 SCIE EI CSCD 1998年第6期597-607,共11页
A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification.... A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition. 展开更多
关键词 Program synthesis very high-level language parallelism and concurrency formal specification first-order logic.
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部