期刊文献+
共找到41篇文章
< 1 2 3 >
每页显示 20 50 100
Clause-based enhancing mode for tableau algorithm for ALCN
1
作者 古华茂 石锦芹 高济 《Journal of Southeast University(English Edition)》 EI CAS 2008年第3期361-364,共4页
As the tableau algorithm would produce a lot of description overlaps when judging the satisfiabilities of concepts(thus wasting much space),a clause-based enhancing mode designed for the language ALCN is proposed.Th... As the tableau algorithm would produce a lot of description overlaps when judging the satisfiabilities of concepts(thus wasting much space),a clause-based enhancing mode designed for the language ALCN is proposed.This enhancing mode constructs a disjunctive normal form on concept expressions and keeps only one conjunctive clause,and then substitutes the obtained succinctest conjunctive clause for sub-concepts set in the labeling of nodes of a completion tree constructed by the tableau algorithm (such a process may be repeated as many times as needed).Due to the avoidance of tremendous descriptions redundancies caused by applying ∩- and ∪-rules of the ordinary tableau algorithm,this mode greatly improves the spatial performance as a result.An example is given to demonstrate the application of this enhancing mode and its reduction in the cost of space. Results show that the improvement is very outstanding. 展开更多
关键词 tableau algorithm enhancing mode CLAUSE SATISFIABILITY
在线阅读 下载PDF
动态描述逻辑的Tableau判定算法 被引量:41
2
作者 常亮 史忠植 +1 位作者 邱莉榕 林芬 《计算机学报》 EI CSCD 北大核心 2008年第6期896-909,共14页
动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动... 动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法. 展开更多
关键词 动态描述逻辑 动作理论 可满足性问题 tableau算法 可判定性
在线阅读 下载PDF
从ALC到SHOQ(D):描述逻辑及其Tableau算法 被引量:34
3
作者 梅婧 林作铨 《计算机科学》 CSCD 北大核心 2005年第3期1-11,35,共12页
描述逻辑是一类知识表示的形式系统,并成为语义Web的逻辑基础。Tableau是描述逻辑的基本证明论,基于Tableau的算法提供了描述逻辑的推理机。本文系统地阐述了对应于语义Web语言从基本的ALC到SHOQ(D)的描述逻辑基础及其相应的Tableau算法。
关键词 ALC 描述逻辑 tableau算法 语义WEB 知识表示
在线阅读 下载PDF
时态描述逻辑ALC-LTL的Tableau判定算法 被引量:5
4
作者 常亮 王娟 +1 位作者 古天龙 董荣胜 《计算机科学》 CSCD 北大核心 2011年第8期150-154,共5页
时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑... 时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-LTL中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。 展开更多
关键词 时态描述逻辑 线性时态逻辑 可满足性问题 tableau算法 复杂度
在线阅读 下载PDF
Tableau算法的优化及模型规约技术 被引量:4
5
作者 刘大有 赖永 王生生 《计算机学报》 EI CSCD 北大核心 2014年第8期1647-1657,共11页
为了近一步提高模态逻辑推理机的效率,提出了两种Tableau算法优化技术——冲突技术和矛盾学习技术,并结合这两种技术实现了针对模态逻辑S4的推理机S4P.在此基础上,为了从Tableau算法生成的模型图中构造一个规模较小的模型,又提出通用模... 为了近一步提高模态逻辑推理机的效率,提出了两种Tableau算法优化技术——冲突技术和矛盾学习技术,并结合这两种技术实现了针对模态逻辑S4的推理机S4P.在此基础上,为了从Tableau算法生成的模型图中构造一个规模较小的模型,又提出通用模型的概念,然后给出通用模型的规约技术并证明该技术对于任意依赖于公理D、T、B、4和5中部分或全部公理的正规模态逻辑的正确性.最后,使用逻辑工作台测试用例对S4P的效率进行测试,实验结果表明S4P的效率优于RACER和FACT++;同时,对S4P生成的测试用例中非有效公式的否定对应的通用模型进行规约,实验结果表明通过模型规约能明显地缩减模型的规模. 展开更多
关键词 模态逻辑 tableau算法 优化 模型规约
在线阅读 下载PDF
Tableau算法在粗逻辑知识推理中的应用 被引量:3
6
作者 阎红灿 闫宏图 刘保相 《贵州师范大学学报(自然科学版)》 CAS 2013年第1期40-43,共4页
Tableau算法是本体推理部分描述逻辑中用于ABox一致性检验的算法,基于二值逻辑,不能完成多值概念的一致性检测。将粗糙逻辑的基本思想植入描述逻辑体系中,并改进了Tableau算法,使粗糙描述逻辑能够完成对粗糙概念的推理任务,为基于语义... Tableau算法是本体推理部分描述逻辑中用于ABox一致性检验的算法,基于二值逻辑,不能完成多值概念的一致性检测。将粗糙逻辑的基本思想植入描述逻辑体系中,并改进了Tableau算法,使粗糙描述逻辑能够完成对粗糙概念的推理任务,为基于语义的本体知识检索奠定了技术基础。 展开更多
关键词 描述逻辑 粗糙逻辑 Tuableau算法 知识推理
在线阅读 下载PDF
ALC中的Tableau算法及其性质 被引量:5
7
作者 段跃兴 《计算机应用与软件》 CSCD 2010年第10期272-274,共3页
描述逻辑是一族知识表示的形式化语言,是一阶谓词逻辑的可判定子集,已成为语义Web的理论基础。描述逻辑中ALC是最小命题封闭的,是其它描述语言的基础,而可判定是描述逻辑的最重要的问题,在ALC中Tableau算法巧妙地解决了这一问题,掌握AL... 描述逻辑是一族知识表示的形式化语言,是一阶谓词逻辑的可判定子集,已成为语义Web的理论基础。描述逻辑中ALC是最小命题封闭的,是其它描述语言的基础,而可判定是描述逻辑的最重要的问题,在ALC中Tableau算法巧妙地解决了这一问题,掌握ALC中的Tableau算法是理解各种描述逻辑中可判定性的基础。对ALC中的Tableau算法进行详细阐述,并对其关键的几个性质:可终止性、完备性和判定性给出了证明,为研究SHOIN(D)中的Tableau算法及性质奠定了基础。 展开更多
关键词 描述逻辑 tableau算法 语义WEB ALC
在线阅读 下载PDF
模块化本体的Tableau算法及其性能优化
8
作者 蒋宗华 徐勇 《计算机工程》 CAS CSCD 2012年第13期289-292,共4页
针对现有模块化本体推理方法通用性低、控制复杂等不足,提出一种基于服务的分布式Tableau算法。模块在进行一致性推理时,对关于外部概念的断言,将调用相应模块的服务进行推理,同一推理中的矛盾在定义相应概念的模块中得到捕获,采用优化... 针对现有模块化本体推理方法通用性低、控制复杂等不足,提出一种基于服务的分布式Tableau算法。模块在进行一致性推理时,对关于外部概念的断言,将调用相应模块的服务进行推理,同一推理中的矛盾在定义相应概念的模块中得到捕获,采用优化技术改进算法的时间性能。实验结果表明,该算法使得模块在表述知识时能灵活引用外部概念,支持复杂的推理任务,具有较好的可伸缩性。 展开更多
关键词 本体 描述逻辑 模块化 本体推理 分布式算法 tableau算法
在线阅读 下载PDF
Tableau-based算法的改进与有限步终止定理
9
作者 王国俊 李璧镜 《陕西师范大学学报(自然科学版)》 CAS CSCD 北大核心 2008年第6期1-4,9,共5页
对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这个新算法,证明了ALCN语言中Abox的相容性可通过标准tableau-ba... 对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这个新算法,证明了ALCN语言中Abox的相容性可通过标准tableau-based算法在有限步之内判定. 展开更多
关键词 描述逻辑 Abox tableau-based算法 标准tableau-based算法 有限步终止定理
在线阅读 下载PDF
一种扩展的动态描述逻辑语言及其Tableau算法 被引量:2
10
作者 郝国舜 马世龙 眭跃飞 《智能系统学报》 2009年第3期226-233,共8页
对动态系统的描述是智能领域的一个重要问题,但目前已有的动态描述逻辑语言,用不可再分的符号表示原子动作,不能区分动作类和动作实例,不足以对实际系统中的动作进行表达.因此提出了一个扩展的动态描述逻辑语言,在原子动作模态词的形式... 对动态系统的描述是智能领域的一个重要问题,但目前已有的动态描述逻辑语言,用不可再分的符号表示原子动作,不能区分动作类和动作实例,不足以对实际系统中的动作进行表达.因此提出了一个扩展的动态描述逻辑语言,在原子动作模态词的形式中可以表示动作的属性,从而区分了一类动作和具体动作.通过对可达关系进行限制,定义了此特殊形式模态词动作的语义.另外,还提供了此语言的Tableau算法,并证明了此算法的可终止性和完备性. 展开更多
关键词 动态描述逻辑 模态逻辑 动态逻辑 tableau算法
在线阅读 下载PDF
一阶自由变元tableau实现过程分析
11
作者 杨杰 《科学技术创新》 2020年第32期99-100,共2页
基于M.C.Fitting研究基础通过改进对应的算法,来进行算法的正确性评估,最后基于实验基础上进一步验证了系统的可靠性,得出优化后的系统算法具有较高的适用性和价值。
关键词 tableau 一阶逻辑 算法
在线阅读 下载PDF
基于Tableau算法的本体模型验证方法研究 被引量:1
12
作者 兰天 程继红 《舰船电子工程》 2011年第10期134-138,共5页
文章首先介绍了本体模型的Tbox术语检验和Abox实例检验,将本体模型的一致性检验简化为术语的可满足性检验。通过引入Tableau算法的思想,对本体模型的概念定义以及概念间的关系进行可满足性测试,最后采用Racer推理机结合海军军械保障实... 文章首先介绍了本体模型的Tbox术语检验和Abox实例检验,将本体模型的一致性检验简化为术语的可满足性检验。通过引入Tableau算法的思想,对本体模型的概念定义以及概念间的关系进行可满足性测试,最后采用Racer推理机结合海军军械保障实例对基于描述逻辑的本体模型可满足性检验的有效性算法进行了验证。 展开更多
关键词 本体模型 tableau算法 Racer推理机
在线阅读 下载PDF
粗描述逻辑RALCQ的Tableau推理
13
作者 许禾 苗长运 《电脑与电信》 2009年第12期73-75,共3页
基于描述逻辑ALCQ,通过引入分级近似算子而得到粗描述逻辑RALCQ。随后通过转换的方法得到粗描述逻辑RALCQ的Tableau算法推理规则及推理复杂性。
关键词 描述逻辑 粗描述逻辑 RALCQ tableau算法
在线阅读 下载PDF
Tableau算法在粗糙描述逻辑中的扩展应用
14
作者 闫之焕 《计算机技术与发展》 2015年第12期10-13,共4页
Tableau算法是描述逻辑中判断概念的可满足性最常用的方法,但传统的Tableau算法只适用于标准的描述逻辑。对于粗糙描述逻辑的情况,有的学者是把粗糙描述逻辑先通过一个转换函数转换为标准描述逻辑,然后再用Tableau算法实现推理,这就需要... Tableau算法是描述逻辑中判断概念的可满足性最常用的方法,但传统的Tableau算法只适用于标准的描述逻辑。对于粗糙描述逻辑的情况,有的学者是把粗糙描述逻辑先通过一个转换函数转换为标准描述逻辑,然后再用Tableau算法实现推理,这就需要在Tableau算法中增加一些规则,这增加了算法不必要的工作。文中给出了粗糙描述逻辑中概念包含关系的一种新的推理的Tableau算法,在这种改进的算法中只需用到概念的子概念和出现在概念中的角色就可以判断一个概念的可满足性,并证明了它的正确性,通过实例说明了它的有效性。 展开更多
关键词 粗糙集 等价关系 描述逻辑 tableau算法
在线阅读 下载PDF
Fuzzy description logic based on vague sets
15
作者 马宗民 王海龙 +1 位作者 严丽 赵法信 《Journal of Southeast University(English Edition)》 EI CAS 2007年第3期399-402,共4页
To enable the representation and reasoning for fuzzy ontologies with expressive fuzzy knowledge on the semantic web, a new fuzzy extension of description logics called vague ALC which is based on vague sets is present... To enable the representation and reasoning for fuzzy ontologies with expressive fuzzy knowledge on the semantic web, a new fuzzy extension of description logics called vague ALC which is based on vague sets is presented. The definition of vague set is introduced and then the syntax and semantics of vague ALC are formally defined. The forms of axioms and assertions in the vague ALC knowledge bases are specified. Finally, the tableau algorithm is developed for the reasoning in the vague ALC. The vague ALC based on vague set uses two degrees of membership instead of a single membership degree in the fuzzy sets and is more accurate in representing the imprecision in the degrees of membership. The vague ALC has more expressive power than ALC and can represent fuzzy knowledge and perform reasoning tasks based on them. Therefore, the vague ALC can enable the representation and reasoning for fuzzy ontologies with expressive fuzzy knowledge on the semantic web. 展开更多
关键词 semantic web description logic fuzzy logic vague sets tableau algorithm
在线阅读 下载PDF
基于OWL的仿真想定本体构建方法 被引量:10
16
作者 庞天亮 袁修久 +2 位作者 赵学军 扈登贵 常永昌 《空军工程大学学报(自然科学版)》 CSCD 北大核心 2012年第6期35-39,共5页
研究了作战过程,提出了基于OWL的作战单元本体、装备本体、任务本体和仿真想定本体的构建方法,采用了描述逻辑对作战相关概念、关系进行了推理,检验了概念、关系的一致性,优化了概念层次结构。通过实例分析,对构建的本体进行了检验。结... 研究了作战过程,提出了基于OWL的作战单元本体、装备本体、任务本体和仿真想定本体的构建方法,采用了描述逻辑对作战相关概念、关系进行了推理,检验了概念、关系的一致性,优化了概念层次结构。通过实例分析,对构建的本体进行了检验。结果表明:该方法实现了军事领域概念的合理分类和想定数据语义的智能检测,可为想定开发人员自动地提供决策支持。 展开更多
关键词 仿真想定 网络本体语言 PROTÉGÉ 描述逻辑 表算法
在线阅读 下载PDF
一类扩展的动态描述逻辑 被引量:23
17
作者 常亮 史忠植 +1 位作者 陈立民 牛温佳 《软件学报》 EI CSCD 北大核心 2010年第1期1-13,共13页
作为描述逻辑的扩展,动态描述逻辑为语义Web服务的建模和推理提供了一种有效途径.在将语义Web服务建模为动作之后,动态描述逻辑从动作执行结果的角度提供了丰富的推理机制,但对于动作的执行过程却不能加以处理.借鉴Pratt关于命题动态逻... 作为描述逻辑的扩展,动态描述逻辑为语义Web服务的建模和推理提供了一种有效途径.在将语义Web服务建模为动作之后,动态描述逻辑从动作执行结果的角度提供了丰富的推理机制,但对于动作的执行过程却不能加以处理.借鉴Pratt关于命题动态逻辑的相关研究,一方面,对动态描述逻辑中动作的语义重新进行定义,将每个动作解释为由关于可能世界的序列组成的集合;另一方面,在动态描述逻辑中引入动作过程断言,用来对动作的执行过程加以刻画.在此基础上提出一类扩展的动态描述逻辑EDDL(X),其中的X表示从ALC(attributive language with complements)到SHOIN(D)等具有不同描述能力的描述逻辑.以X为描述逻辑ALCQO(attributive language with complements,qualified number restrictions and nominals)的情况为例,给出了EDDL(ALCQO)的表判定算法,并证明了算法的可终止性、可靠性和完备性.EDDL(X)可以从动作执行过程和动作执行结果两个方面对动作进行全面的刻画和推理,为语义Web服务的建模和推理提供了进一步的逻辑支持. 展开更多
关键词 动态描述逻辑 动作推理 动作的执行过程 表判定算法 语义WEB服务
在线阅读 下载PDF
一种带传递关系的认知描述逻辑研究 被引量:4
18
作者 曹逸 徐德智 +1 位作者 陈建二 管庆华 《计算机研究与发展》 EI CSCD 北大核心 2009年第3期452-458,共7页
描述逻辑是语义Web的逻辑基础,它是形式化表达领域知识的一种工具.描述逻辑是一阶逻辑的可判定子集,适合对领域知识的概念术语进行建模.因为某些应用程序的需要和领域知识难以完全描述的因素,Web上有大量的不完全知识.描述逻辑基于开放... 描述逻辑是语义Web的逻辑基础,它是形式化表达领域知识的一种工具.描述逻辑是一阶逻辑的可判定子集,适合对领域知识的概念术语进行建模.因为某些应用程序的需要和领域知识难以完全描述的因素,Web上有大量的不完全知识.描述逻辑基于开放世界假设,只能表达单调推理,不能处理不完全知识.在描述逻辑中加入认知运算符K可以得到认知描述逻辑.认知描述逻辑因其非单调特性和良好的时间复杂度等特点在处理不完全知识方面有较好的优势.在认知描述逻辑ALCK的基础上加入传递关系属性提出了新的认知描述逻辑语言ALCKR+,保留了描述逻辑原有的优点,增强了表达能力并通过认知查询拥有了非单调推理的能力.设计了ALCKR+的语法、语义以及表算法,给出了表算法的正确性以及可判定性证明,证明表算法的时间复杂度为PSPACE-complete. 展开更多
关键词 描述逻辑 认知描述逻辑 传递关系 认知查询 表算法
在线阅读 下载PDF
动态描述逻辑推理的并行计算技术 被引量:3
19
作者 王竹晓 胡宏 +1 位作者 陈立民 史忠植 《计算机研究与发展》 EI CSCD 北大核心 2011年第12期2317-2325,共9页
在设计用于处理大规模本体和数据的推理引擎时,推理引擎的可扩展性是一个需要研究的重要问题.动态描述逻辑要在真实环境中获得成功应用,需要在推理中采用并行计算技术.提出了两种方法将并行计算技术应用于动态描述逻辑推理.方法1是设计... 在设计用于处理大规模本体和数据的推理引擎时,推理引擎的可扩展性是一个需要研究的重要问题.动态描述逻辑要在真实环境中获得成功应用,需要在推理中采用并行计算技术.提出了两种方法将并行计算技术应用于动态描述逻辑推理.方法1是设计分布式动态描述逻辑框架.分布式动态描述逻辑由若干独立的动态描述逻辑所组成,这些动态描述逻辑两两之间通过桥规则联系起来.提出了基于Tableau的分布式推理算法,从而为分布式动态描述逻辑提供了全局推理能力,并且该算法可以将大的推理任务分解为若干子任务,而这些子任务可以被不同的推理主体并行处理.方法2是并行化动态描述逻辑的Tableau算法的不确定分支.不确定分支的并行计算使得推理任务可以在若干独立机器上同时执行.最后,介绍了推理引擎的原型实现并评估了其性能.实验结果表明提出的两种方法取得了明显的推理加速效果. 展开更多
关键词 并行推理 动态描述逻辑 分布式动态描述逻辑 表算法 推理引擎
在线阅读 下载PDF
可判定的时序动态描述逻辑 被引量:6
20
作者 常亮 史忠植 +1 位作者 古天龙 王晓峰 《软件学报》 EI CSCD 北大核心 2011年第7期1524-1537,共14页
动态描述逻辑DDL(dynamic description logic)提供了一种基于描述逻辑的动作理论,适用于语义Web环境下对动态领域知识的刻画和推理.为了将分支时序逻辑的刻画能力引入到动态描述逻辑中,将时间的进展体现为原子动作的执行,从而将时序维... 动态描述逻辑DDL(dynamic description logic)提供了一种基于描述逻辑的动作理论,适用于语义Web环境下对动态领域知识的刻画和推理.为了将分支时序逻辑的刻画能力引入到动态描述逻辑中,将时间的进展体现为原子动作的执行,从而将时序维与动态维统一起来.在此基础上,从描述逻辑ALCQIO出发构建了一个时序动态描述逻辑TDALCQIO,给出了TDALCQIO的Tableau判定算法,并证明了算法的可终止性和正确性.TDALCQIO不仅兼容了构建在描述逻辑ALCQIO基础上的动态描述逻辑的刻画和推理能力,而且还可从可达性、安全性等角度对整个动态领域的时序特征进行刻画和推理,从而为语义Web环境下对动态领域知识的刻画和推理提供了进一步的逻辑支持. 展开更多
关键词 动态描述逻辑 分支时序逻辑 知识表示和推理 动作理论 tableau判定算法
在线阅读 下载PDF
上一页 1 2 3 下一页 到第
使用帮助 返回顶部