论文部分内容阅读
对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这个新算法,证明了ALCN语言中Abox的相容性可通过标准tableau-based算法在有限步之内判定.
Tableau-based算法的改进与有限步终止定理
【摘 要】
：
对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这
【机 构】
：
陕西师范大学数学与信息科学学院
【出 处】
：
陕西师范大学学报(自然科学版)
【发表日期】
：
2008年6期
其他文献
目的：为减少错误处方，提高书写处方合格率及合理的用药水平。方法：对中铁十七局中心医院2011年1～4月的不合理处方进行整理，并分析其存在的问题。结果：不合理处方主要表面在书写不规
研究了模态逻辑系统S5中的析（合）取范式定理的归纳证明，给出了在S5中用深度至多等于1的最简模态公式通过析取与合取运算表示含有多重模态词的公式的方法．作为范式定理的应用，讨论
研究了连续Quantale及其范畴性质,定义了半连续Quantale,在此基础上讨论了半连续Quantale、连续Quantale和正则Quantale之间的关系.证明了严格右侧的连续Quantale是正则Quant
<正> 宝钢2030mm 冷连轧机是国内第1台由西德引进的全连续轧机,其轧制规程有一定特点。在进行道次计算时,轧制规范是进行压下负荷分配的重要依据。轧制规范选择得好,不仅可获
探讨了逻辑度量空间的结构,证明了在经典逻辑度量空间上存在一种反射变换φ,且φ保持逻辑等价关系不变,并且是同态映射;φ自然导出Lindenbaum代数上的一个反射变换φ*,φ*是L
【正】不发酵糖菌是指一大群不发酵葡萄糖或仅以氧化形式利用葡萄糖的需氧或兼性厌氧、无芽胞的革兰阴性杆菌,广泛存在于自然界的土壤、水、物体表面和空气中,大多为条件致病
首先,我以极喜悦的心情热烈祝贺中国药理学会成立30周年!中国药理学会的成立,是由我国药理学界著名和知名的老一辈药理学先导药理学家,经较长时期的、以坚韧的精神不断地努力
在气缸盖导管孔的加工中普遍使用两种刀具，即传统的套式铰刀和带导条可调精铰刀。如图1所示的刀具，对于加工像导管孔这样的深孔，前者因为刀杆较细且无导向支撑，铰出孔表面粗糙度
中华文明根植于农耕文化,乡村是中华文明的基本载体,许多珍贵的非物质文化遗产散落在乡间。近年来,随着城镇化进程的加快,农村空心化、农民老龄化等问题日益凸显。文章以南通