期刊文献+
共找到51篇文章
< 1 2 3 >
每页显示 20 50 100
从经典逻辑知识构建ASP知识库的新方法 被引量:6
1
作者 赵岭忠 王雪松 +1 位作者 钱俊彦 蔡国永 《计算机应用》 CSCD 北大核心 2010年第11期2932-2936,共5页
回答集程序设计(ASP)是一种主流的非单调知识表示工具。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识,给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法,并以实例说明了其有... 回答集程序设计(ASP)是一种主流的非单调知识表示工具。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识,给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法,并以实例说明了其有效性。该方法满足转化后ASP程序的回答集与原公式集的模型具有一一对应关系。在实际应用中,该方法提供了一项从现存的以谓词逻辑为表示语言的知识库,构建以ASP为知识表示语言的非单调知识库的技术。 展开更多
关键词 谓词逻辑 谓词公式 回答集程序设计 asp知识库
下载PDF
基于ASP的CSP模型验证性质反例生成技术研究 被引量:3
2
作者 王雪松 赵岭忠 张超 《计算机应用研究》 CSCD 北大核心 2013年第1期52-55,共4页
为了解决当前通信顺序进程(CSP)模型检测不支持在验证工具的一次运行中验证多个性质的问题,建立了基于ASP的CSP并发模型验证框架。主要研究在该框架下当待验证的系统性质不满足时生成相应性质反例的技术。把ASP程序调试中的ASP程序支撑... 为了解决当前通信顺序进程(CSP)模型检测不支持在验证工具的一次运行中验证多个性质的问题,建立了基于ASP的CSP并发模型验证框架。主要研究在该框架下当待验证的系统性质不满足时生成相应性质反例的技术。把ASP程序调试中的ASP程序支撑原因分析技术应用于该问题的研究,提出了相应的反例生成算法,实例表明了该算法的正确性。 展开更多
关键词 通信顺序进程 回答集编程 支撑原因
下载PDF
云资源调度的回答集程序描述性求解
3
作者 王卫舵 王以松 杨磊 《广西师范大学学报(自然科学版)》 CAS 北大核心 2024年第2期94-104,共11页
针对求解难度为NP完全的基础设施即服务(IaaS)模式云资源调度问题,本文提出一种基于回答集程序(ASP)的描述性优化求解方法,并对其正确性进行分析。首先,把满足虚拟机CPU使用的情况下关闭尽可能多的主机做为减少云平台能耗的方法,将云资... 针对求解难度为NP完全的基础设施即服务(IaaS)模式云资源调度问题,本文提出一种基于回答集程序(ASP)的描述性优化求解方法,并对其正确性进行分析。首先,把满足虚拟机CPU使用的情况下关闭尽可能多的主机做为减少云平台能耗的方法,将云资源调度问题形式化表述;其次,结合形式化描述以及减少云平台能耗的策略,将云资源调度问题用ASP编码为描述性(优化)问题,并分析其正确性;最后,在公开的PlanetLab数据集上进行实验,结果显示,ASP方法可在保障服务质量的同时减少集群能耗,最高可节能13%以上。这表明ASP方法在云资源调度问题上是有效的,从而提供一种易理解、易修改并能充分利用ASP最新工具成果的有效云资源调度新方法。 展开更多
关键词 回答集程序 云资源调度 多目标优化 约束满足问题 能耗
下载PDF
基于ASP的CSP并发系统验证研究 被引量:4
4
作者 赵岭忠 张超 钱俊彦 《计算机科学》 CSCD 北大核心 2012年第12期125-132,共8页
传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为... 传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。 展开更多
关键词 通信顺序进程 回答集编程 LTL CTL
下载PDF
基于关键迹和ASP的CSP模型检测 被引量:3
5
作者 赵岭忠 翟仲毅 +1 位作者 钱俊彦 郭云川 《软件学报》 EI CSCD 北大核心 2015年第10期2521-2544,共24页
模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有... 模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例. 展开更多
关键词 模型检测 通信顺序进程 关键迹模型 线性时态逻辑 回答集程序设计
下载PDF
基于ASP的程序切片 被引量:2
6
作者 翟仲毅 王雪松 赵岭忠 《桂林电子科技大学学报》 2012年第1期29-34,共6页
针对程序切片在程序理解和程序测试方面的应用,提出了一种基于ASP的程序切片方法。ASP是一种声明性问题解决方法,它可以高效地描述程序切片问题。基于ASP的切片方法,可以把切片的查找转化为回答集的求解。另外,对传统数据流切片算法进... 针对程序切片在程序理解和程序测试方面的应用,提出了一种基于ASP的程序切片方法。ASP是一种声明性问题解决方法,它可以高效地描述程序切片问题。基于ASP的切片方法,可以把切片的查找转化为回答集的求解。另外,对传统数据流切片算法进行了改进;改进后的算法可以减少重复计算,提高了运行效率。通过实验表明了此改进法的正确性和高效性;并且比较了3种ASP求解器(DLV、Smodels、Cmodels)的执行效率,基于Cmod-els的改进算法的运行效率是最高的。 展开更多
关键词 程序切片 数据流 回答集编程
下载PDF
基于粗糙集与ASP的变压器故障诊断 被引量:2
7
作者 侯权 赵岭忠 熊远武 《桂林电子科技大学学报》 2017年第2期147-153,共7页
针对传统电力变压器故障诊断方法无法获取完备故障信息、加入新约束条件需重新构建系统模型,提出一种基于粗糙集理论和ASP的电力变压器故障诊断方法。利用粗糙集理论对变压器油溶解的气体进行分析,结合ASP规则将待求解的问题转化为ASP... 针对传统电力变压器故障诊断方法无法获取完备故障信息、加入新约束条件需重新构建系统模型,提出一种基于粗糙集理论和ASP的电力变压器故障诊断方法。利用粗糙集理论对变压器油溶解的气体进行分析,结合ASP规则将待求解的问题转化为ASP知识库,通过ASP求解器实现故障诊断。与传统方法相比,该诊断技术简洁精确,模型表达能力强,具有一定的灵活性和容错能力,可以实现知识库的动态维护,变压器故障诊断准确率可达94.8%。 展开更多
关键词 粗糙集理论 回答集程序 知识库 动态维护
下载PDF
一种用于Slater与Kemeny选举求解的ASP方法 被引量:3
8
作者 徐珩僭 王以松 冯仁艳 《计算机工程》 CAS CSCD 北大核心 2019年第9期198-203,共6页
针对求解复杂度为NP难问题的Slater选举,提出一种回答集程序设计(ASP)方法用于求解选举结果。通过ASP构造尽可能少的无回路锦标赛,找到与原锦标赛差别最小的一个并从中选出获胜者。实验结果表明,该方法的编码方式不依赖于候选人的数量,... 针对求解复杂度为NP难问题的Slater选举,提出一种回答集程序设计(ASP)方法用于求解选举结果。通过ASP构造尽可能少的无回路锦标赛,找到与原锦标赛差别最小的一个并从中选出获胜者。实验结果表明,该方法的编码方式不依赖于候选人的数量,时间复杂度低,可读性强,并且适用于Kemeny选举。 展开更多
关键词 Slater选举 Kemeny选举 NP难问题 回答集程序设计 锦标赛
下载PDF
一种基于ILP和ASP的学习B语言描述的动作模型方法 被引量:1
9
作者 刘振 张志政 《计算机科学》 CSCD 北大核心 2015年第1期220-226,共7页
动作模型学习可以使Agent主动适应动态环境中的变化,从而提高Agent的自治性,同时也可为动态域建模提供一个初步模型,为后期的模型完善和修改提供了基础。通过结合归纳逻辑程序设计(Inductive Logic Programming,ILP)和回答集程序设计(An... 动作模型学习可以使Agent主动适应动态环境中的变化,从而提高Agent的自治性,同时也可为动态域建模提供一个初步模型,为后期的模型完善和修改提供了基础。通过结合归纳逻辑程序设计(Inductive Logic Programming,ILP)和回答集程序设计(Answer Set Programming,ASP),设计了一个学习B语言描述的动作模型算法,该算法可以在混合规模的动态域中进行学习,并采用经典规划实例验证了该学习算法的有效性。 展开更多
关键词 动作模型学习 动作语言B 归纳逻辑程序设计 回答集逻辑程序设计
下载PDF
基于启发式搜索的ASP程序支撑原因分析算法
10
作者 董凤娇 王雪松 +1 位作者 赵岭忠 张超 《桂林电子科技大学学报》 2012年第3期222-226,共5页
为了尽快找到一个错误及其来源,以加快ASP程序调试的效率,把启发式搜索技术引入ASP程序支撑原因分析算法。在生成支撑原因分析图时利用启发式函数,仅搜索对回答集产生影响且有可能更快找到一个支撑原因的规则。改进算法在搜索关于某个... 为了尽快找到一个错误及其来源,以加快ASP程序调试的效率,把启发式搜索技术引入ASP程序支撑原因分析算法。在生成支撑原因分析图时利用启发式函数,仅搜索对回答集产生影响且有可能更快找到一个支撑原因的规则。改进算法在搜索关于某个回答集的支撑原因时,其时间和空间复杂度明显下降。实例分析表明了该算法的有效性。 展开更多
关键词 asp程序 justification图 回答集 启发式算法
下载PDF
基于ASP及稳定失败语义的CSP模型检测
11
作者 左贵征 赵岭忠 《桂林电子科技大学学报》 2015年第5期401-407,共7页
针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实... 针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。 展开更多
关键词 通信顺序进程 线性时态逻辑 稳定失败语义 回答集程序设计
下载PDF
基于ASP的中间人协商模型
12
作者 张俊琴 赵岭忠 《桂林电子科技大学学报》 2017年第5期411-416,共6页
针对顺序协商模型中的资源浪费问题,以及电子商务中间人模型的适用性低问题,提出一个基于ASP的中间人协商模型。利用回答集给出了协商建议的形式化描述,结合ASP规则将中间agent的功能转化为ASP知识库,通过ASP求解器实现协商过程。实验... 针对顺序协商模型中的资源浪费问题,以及电子商务中间人模型的适用性低问题,提出一个基于ASP的中间人协商模型。利用回答集给出了协商建议的形式化描述,结合ASP规则将中间agent的功能转化为ASP知识库,通过ASP求解器实现协商过程。实验结果表明,与顺序协商模型相比,该模型可有效解决顺序协商中的资源浪费问题,且提高了协商效率;与电子商务中间人模型相比,该模型可用于非数字形式的协商元素的协商。 展开更多
关键词 中间人协商 回答集程序设计 中间agent
下载PDF
析取回答集程序设计结构化测试方法 被引量:1
13
作者 杨东 王以松 《计算机应用》 CSCD 北大核心 2023年第1期215-220,共6页
针对析取回答集程序的结构化测试基础理论匮乏的问题,系统化地提出析取回答集程序结构化测试覆盖的概念。首先,定义针对析取回答集程序的测试用例,确立析取回答集程序的主要测试实体为程序中的逻辑规则;其次,通过对规则的头、规则的体... 针对析取回答集程序的结构化测试基础理论匮乏的问题,系统化地提出析取回答集程序结构化测试覆盖的概念。首先,定义针对析取回答集程序的测试用例,确立析取回答集程序的主要测试实体为程序中的逻辑规则;其次,通过对规则的头、规则的体、规则的集合等不同测试目标构建了规则覆盖、定义覆盖、环覆盖等基本概念来模拟结构化测试中的语句覆盖、分支覆盖等概念;最后,提出了析取回答集程序的测试覆盖率计算公式,并举例说明各种覆盖下的覆盖率计算方法,并讨论了析取回答集程序的部分特殊性质和关键指标。 展开更多
关键词 回答集程序设计 测试理论 析取回答集程序 结构化测试方法 覆盖
下载PDF
A characterization of answer sets for logic programs 被引量:1
14
作者 ZHANG MingYi ZHANG Ying FangZhen LiN 《Science in China(Series F)》 2007年第1期46-62,共17页
Checking if a program has an answer set, and if so, compute its answer sets are just some of the important problems In answer set logic progremming. Solving these problems using Gelfond and Llfschltz's original defin... Checking if a program has an answer set, and if so, compute its answer sets are just some of the important problems In answer set logic progremming. Solving these problems using Gelfond and Llfschltz's original definition of answer sets Is not an easy task. Alternative charaoterlzatlons of answer sets for nested logic programs by Erdem and Llfschltz, Lee and Llfschltz, and You at el. are based on the completion semantics and various notions of tlghtnese. However, the notion of tightness Is a local notion In the sense that for different answer sets there are, In general, different level mappings capturing their tlghtnese. This makes It hard to be used In the deelgn of algorithms for computing answer sets. This paper proposes a charecterization of answer sets based on sets of generetlng rules. From this charaoterlzation new algorithms are derived for computing answer sets and for performing some other reasoning teaks. As an application of the charecterlzatlon a sufficient and necessary condition for the equivalence between answer set sementics and completion semantics has been proven, and a basic theorem Is shown on computing answer sets for nested logic programs baaed on an extended notion of loop formulas. These results on tlghtnese and loop formulas are more general than that in You and Lin'a work. 展开更多
关键词 nested logic programming characterization of answer sets completion semantics TIGHTNESS loop formulas
原文传递
一种支持个性化协调的服务机器人体系结构 被引量:8
15
作者 吉建民 陈小平 +2 位作者 姜节汇 靳国强 王锋 《南京大学学报(自然科学版)》 CAS CSCD 北大核心 2010年第2期131-139,共9页
本文提出一种支持个性化协调的服务机器人体系结构(individualized coordination architecture,ICA).主要动机是通过自然语言人机对话获取用户的个人特性和其他信息,通过对这些信息进行自动推理和规划,实现利用个人特性的自动问题求解,... 本文提出一种支持个性化协调的服务机器人体系结构(individualized coordination architecture,ICA).主要动机是通过自然语言人机对话获取用户的个人特性和其他信息,通过对这些信息进行自动推理和规划,实现利用个人特性的自动问题求解,并满足家庭环境对服务机器人的应用要求.本文着重介绍ICA的主要部件的功能及其相互衔接方式,描述任务规划的机制和实现手段,并通过一个实例说明在一个初步实现的原型系统中从自然语言到任务规划的完整过程. 展开更多
关键词 自主机器人 人机协调 个性化 自然语言处理 answer set逻辑程序设计
下载PDF
一种基于事件的Web服务组合方法 被引量:9
16
作者 李鑫 程渤 +1 位作者 杨国纬 刘启和 《软件学报》 EI CSCD 北大核心 2009年第12期3101-3116,共16页
为获得一种既易于实现又能满足用户多样化需求的服务组合的有效途径,提出一种基于事件的服务组合方法.首先定义了一种基于ECA(event-condition-action)规则的语言——简单服务事件语言.在这种语言基础上,通过模块化方法构造的用于描述... 为获得一种既易于实现又能满足用户多样化需求的服务组合的有效途径,提出一种基于事件的服务组合方法.首先定义了一种基于ECA(event-condition-action)规则的语言——简单服务事件语言.在这种语言基础上,通过模块化方法构造的用于描述组合服务的组合方案,不但解决了采用AI规划(artificial intelligent planning)时服务组合域表示困难的问题,而且解决了采用UML(unified modeling language)等技术时描述能力不足的问题.随后,为有效地表示组合方案,完成了它的语义定义以及answer set程序编码工作.最后利用answer set编程(answer set programming)技术实现了对组合轨迹的表示. 展开更多
关键词 简单服务事件语言 answer set编程 组合方案 组合轨迹 前序服务集 互斥约束
下载PDF
E-R模型的回答集编程表示 被引量:7
17
作者 李鑫 李凡 +1 位作者 边杏宾 刘启和 《计算机研究与发展》 EI CSCD 北大核心 2010年第1期164-173,共10页
作为一种广为接受的语义数据模型,E-R模型被广泛地应用于数据库设计阶段.但是E-R模型自身却存在某些缺陷,这些缺陷制约了对其进一步的应用.针对E-R模型的改进,目前主要存在基于图形表示和描述性逻辑表示两种途径.但是,前者仍然不具有自... 作为一种广为接受的语义数据模型,E-R模型被广泛地应用于数据库设计阶段.但是E-R模型自身却存在某些缺陷,这些缺陷制约了对其进一步的应用.针对E-R模型的改进,目前主要存在基于图形表示和描述性逻辑表示两种途径.但是,前者仍然不具有自动推理能力,而后者却存在表示能力弱、与数据库兼容性不足等缺陷.为克服以上缺陷,提出一种利用回答集编程(answer set programming)表示E-R模型的新方法.首先,对应于数据库的E-R模式被区分为基本和扩展两种类型,并分别完成它们的语法与语义定义.其次,利用回答集编程完成以上两类模式的逻辑编程表示.最后,完成表示的正确性证明.提出的方法不仅为E-R模型提供了一种新的逻辑表示途径,而且相对原有的两种E-R模型改进途径具有明显的优势.更为重要的是该研究成果使得应用E-R模型实现异构数据库之间的语义协作成为可能. 展开更多
关键词 E-R模型 回答集编程 基本模式 扩展模式 规则
下载PDF
非一致OWL本体的推理方法研究 被引量:4
18
作者 丁松 唐胜群 +2 位作者 刘坤 张亮 秦学 《计算机工程与应用》 CSCD 北大核心 2011年第9期21-24,共4页
针对目前OWL推理机无法在非一致本体上进行推理的问题,提出了一种基于回答集程序的非一致本体推理方式,将OWL本体翻译为一类逻辑程序:HEX回答集程序,把本体推理问题规约为回答集程序求解问题。并通过在非一致本体上的推理实验,验证了该... 针对目前OWL推理机无法在非一致本体上进行推理的问题,提出了一种基于回答集程序的非一致本体推理方式,将OWL本体翻译为一类逻辑程序:HEX回答集程序,把本体推理问题规约为回答集程序求解问题。并通过在非一致本体上的推理实验,验证了该类方法的有效性。 展开更多
关键词 回答集程序 本体 非单调推理 网络本体语言(OWL) 非一致性 描述逻辑
下载PDF
基于进程迹的CSP模型验证框架 被引量:3
19
作者 赵岭忠 翟仲毅 钱俊彦 《计算机科学》 CSCD 北大核心 2013年第11期181-186,221,共7页
CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框... CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。 展开更多
关键词 通信顺序进程(CSP) 并发系统 迹模型 回答集编程(asp)
下载PDF
概率逻辑程序 被引量:4
20
作者 王洁 鞠实儿 《计算机科学》 CSCD 北大核心 2003年第7期1-3,11,共4页
The purpose of this paper is to present the syntax and semantics of probabilistic logic programming to al-low for the correct representation of incomplete information. General logic programming is extended by a subint... The purpose of this paper is to present the syntax and semantics of probabilistic logic programming to al-low for the correct representation of incomplete information. General logic programming is extended by a subintervalof [0,1] that describes the range for the conditional probability of the head of a clause given the range for the proba-bility of each atom of its body. We define the semantics (answer sets semantics) of such probabilistic logic program-ming and illustrative their applications. We also show some properties of answer sets semantics for the probabilisticlogic programs. 展开更多
关键词 概率逻辑程序 知识描述 知识推理 自动推理
下载PDF
上一页 1 2 3 下一页 到第
使用帮助 返回顶部