期刊文献+
共找到137篇文章
< 1 2 7 >
每页显示 20 50 100
Theory of (n) truth degrees of formulas in modal logic and a consistency theorem 被引量:13
1
作者 WANG GuoJun DUAN QiaoLin 《Science in China(Series F)》 2009年第1期70-83,共14页
The theory of (n) truth degrees of formulas is proposed in modal logic for the first time. A consistency theorem is obtained which says that the (n) truth degree of a modality-free formula equals the truth degree ... The theory of (n) truth degrees of formulas is proposed in modal logic for the first time. A consistency theorem is obtained which says that the (n) truth degree of a modality-free formula equals the truth degree of the formula in two-valued propositional logic. Variations of (n) truth degrees of formulas w.r.t. n in temporal logic is investigated. Moreover, the theory of (n) similarity degrees among modal formulas is proposed and the (n) modal logic metric space is derived therefrom which contains the classical logic metric space as a subspace. Finally, a kind of approximate reasoning theory is proposed in modal logic. 展开更多
关键词 modal logic (n) truth degrees consistency theorem temporal logic (n) modality similarity degrees (n) modality logic metric space approximate reasoning
原文传递
The Global Properties of Valid Formulas in Modal Logic K
2
作者 孙吉贵 程晓春 刘叙华 《Journal of Computer Science & Technology》 SCIE EI CSCD 1996年第6期615-621,共7页
Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal au... Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal automated rea-soning systems, thus the efficiency of the whole system is improved. This paper presents some global properties of valid formulas in modal logic K. Such prop-erties are structure characters of formulas, so they are simple and easy to check.At the same time, some global properties of K unsatisfiable formula set are also given. 展开更多
关键词 modal logic system K global property tableau method automated reasoning
原文传递
基于自动推理技术的智能规划方法 被引量:22
3
作者 吕帅 刘磊 +1 位作者 石莲 李莹 《软件学报》 EI CSCD 北大核心 2009年第5期1226-1240,共15页
对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规... 对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势. 展开更多
关键词 智能规划 命题逻辑 模态逻辑 非单调逻辑 描述逻辑 自动推理 可满足性
下载PDF
面向对象数据库建模方法与逻辑设计 被引量:8
4
作者 刘培玉 刘法胜 +1 位作者 江志超 王新华 《计算机应用研究》 CSCD 1996年第3期39-41,共3页
本文首先给出了一种用于信息建模的对象式系统分析模型,即对象关系模型ORM(Object-RelationModel):其次介绍了对象关系模型的正确性问题;最后介绍了用对象关系模型进行数据库逻辑设计的方法和步骤。这种模... 本文首先给出了一种用于信息建模的对象式系统分析模型,即对象关系模型ORM(Object-RelationModel):其次介绍了对象关系模型的正确性问题;最后介绍了用对象关系模型进行数据库逻辑设计的方法和步骤。这种模型是对实体联系国(E—R图)的扩充,更适合面向对象数据库的设计;又因ORM模型便于图形描述,因而,支持数据库设计信息建模的辅助软件工具也易于开发实现。 展开更多
关键词 数据库 面向对象 建模 逻辑设计
下载PDF
基于模态逻辑D公理系统的Conformant规划方法 被引量:6
5
作者 吕帅 刘磊 +1 位作者 李莹 石莲 《计算机研究与发展》 EI CSCD 北大核心 2009年第7期1160-1168,共9页
2006年,conformant规划问题成为国际规划竞赛不确定性问题域中的标准测试问题,得到研究人员的广泛关注.目前,conformant规划系统都是将其看成信念状态空间上的启发式搜索问题予以求解.通过分析conformant规划问题的语法和语义,提出新的... 2006年,conformant规划问题成为国际规划竞赛不确定性问题域中的标准测试问题,得到研究人员的广泛关注.目前,conformant规划系统都是将其看成信念状态空间上的启发式搜索问题予以求解.通过分析conformant规划问题的语法和语义,提出新的基于模态逻辑的规划框架,将其转换为模态逻辑D公理系统的一系列定理证明问题.提出2种基于模态逻辑的编码方式,构造相应的公理与推理规则形成模态公式集,保证对于D系统的定理证明过程等同于原问题的规划过程,并通过问题实例验证该方法的有效性.继基于SAT、CSP、线性规划、模型检测等求解技术的规划方法后,该规划框架是基于转换的规划方法的一种新的尝试. 展开更多
关键词 conformant规划 模态逻辑 自动推理 可满足性 公理系统 D公理
下载PDF
三次样条曲线拟合的算法及实现 被引量:15
6
作者 郭云 吴松强 李建蜀 《计算机应用研究》 CSCD 1996年第6期41-42,共2页
样条曲线拟合是计算机图形应用的重要方面,本文用泰勒展开式求得分段样条曲线函数,可由用户控制的端点条件.求得通用的拟合算法,并用实例验证了拟合的曲线图形效果。
关键词 样条曲线 曲线拟合 算法 CAD
下载PDF
基于模糊命题模态逻辑的形式推理系统(英文) 被引量:6
7
作者 张再跃 眭跃飞 曹存根 《软件学报》 EI CSCD 北大核心 2005年第8期1359-1365,共7页
探讨基于可信度的模糊命题模态逻辑的形式推理,给出相关的模糊Kripke语义描述.其研究目的旨在解决基于模态命题逻辑的模糊推理的能行问题.在研究过程与方法上,以完全形式化的方法将模糊模态逻辑语法和语义统一在一个形式系统中,以模糊... 探讨基于可信度的模糊命题模态逻辑的形式推理,给出相关的模糊Kripke语义描述.其研究目的旨在解决基于模态命题逻辑的模糊推理的能行问题.在研究过程与方法上,以完全形式化的方法将模糊模态逻辑语法和语义统一在一个形式系统中,以模糊约束作为基本表达式,给出推理规则,建立了相应的模糊推理形式系统,并以形式系统中模糊约束集的可满足性来表示模糊推理的有效性,使模糊推理过程变得容易,为最终在计算机上实现基于模态逻辑的模糊推理打下了一定的基础.主要结论是证明了基于可满足性的模糊推理形式系统的可靠性与完备性. 展开更多
关键词 命题模态逻辑 模糊推理 形式系统
下载PDF
一种新型的数据库应用──数据采掘 被引量:9
8
作者 屈定春 林原 《计算机应用研究》 CSCD 1996年第6期8-11,共4页
本文介绍了数据采掘(DataMining)的基本概念,具体分析了两种数据采掘工具,并讨论了与数据采掘相关的一些技术。
关键词 数据库 应用 数据采掘 数据仓库 数据采集
下载PDF
Windows环境下开发实时系统的尝试 被引量:3
9
作者 彭光正 高赛 李直 《计算机应用》 CSCD 1996年第5期45-47,共3页
针对Windows的非枪先式多任务调度机制使其不适于作为实时系统的支撑环境这一弱点,本文提出了综合改进措施和方法。
关键词 WINDOWS 实时系统 中断 实时操作系统
下载PDF
基于一阶模态逻辑的模糊推理(英文) 被引量:2
10
作者 张晓如 张再跃 +1 位作者 眭跃飞 黄智生 《软件学报》 EI CSCD 北大核心 2008年第12期3170-3178,共9页
研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对... 研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对象是模糊约束,针对模糊约束引进可满足性概念,研究模糊约束可满足性相关性质.利用模糊约束的概念,模糊断言间的推理可以直接在语义环境下加以考虑,因此,以模糊约束为基本元素的模糊推理形式系统随之建立.主要分析新产生断言有效性与模糊约束集可满足性之间的关系,并在此基础上给出了模糊推理形式系统的推理规则.进一步的工作可探讨模糊推理形式系统的可靠性与完全性,建立推理过程的能行机制.研究结果可在人工智能和计算机科学等领域得以应用. 展开更多
关键词 模态逻辑 模糊推理 形式系统 模糊约束 可满足性
下载PDF
Cialdea一阶模态归结系统的不完备性及其改进 被引量:5
11
作者 孙吉贵 刘叙华 《计算机学报》 EI CSCD 北大核心 1995年第6期401-408,共8页
Cialdea的一阶模态D逻辑归结系统具有符号冗余较少和机器上较容易实现等优点,但它是不完备的.本文中,我们改进了Cialdea归结系统,引入了两个可能算子约束的公式间的归结规则,得到了一种新的一阶模态D逻辑的归结系... Cialdea的一阶模态D逻辑归结系统具有符号冗余较少和机器上较容易实现等优点,但它是不完备的.本文中,我们改进了Cialdea归结系统,引入了两个可能算子约束的公式间的归结规则,得到了一种新的一阶模态D逻辑的归结系统,记为FMRD.FMRD很好地保持了Cialdea归结系统的优点,同时,我们证明了FMRD的可靠性与完备性. 展开更多
关键词 FMRD归结 自动推理 模态归结系统 不完备性
下载PDF
模态归结弱包含删除策略 被引量:6
12
作者 孙吉贵 刘叙华 《计算机学报》 EI CSCD 北大核心 1994年第5期321-329,共9页
本文提出了一种模态归结的弱包含删除策略,证明了使用弱包含删除策略模态归结的完备性.从而,将Auffray等人提出的开问题(OpenProblem)——模态归结包含删除策略的完备性向前推进了一步.
关键词 模态归结 弱包含删除 自动推理
下载PDF
Petri网用于表示知识 被引量:18
13
作者 林闯 陆维明 《计算机学报》 EI CSCD 北大核心 1992年第1期1-16,共16页
本文研究了各种级别Petri网与模态逻辑之间的关系.Petri网的Enlogy是研究这些关系的基础.状况(case)和可达(Reachability)概念已经成功地用于以条件/事件(Condition/Event,简称C/E)网作知识表示.本文引用上述两个概念,使位置/变迁(Place... 本文研究了各种级别Petri网与模态逻辑之间的关系.Petri网的Enlogy是研究这些关系的基础.状况(case)和可达(Reachability)概念已经成功地用于以条件/事件(Condition/Event,简称C/E)网作知识表示.本文引用上述两个概念,使位置/变迁(Place/Transition,简称P/T)网和高级Petri网(High Level Petri Net,简称HLPN)可作知识表示.为了增强以 HLPN网作知识表示的能力,我们引用了状况变量和等价状况变量的概念.文中我们还以例子说明这些方法是可用的和有效的. 展开更多
关键词 PETRI网 知识表示 模态逻辑
下载PDF
植物志数据库的信息组织 被引量:6
14
作者 陆纪权 夏瑾 《计算机应用研究》 CSCD 1996年第6期68-70,共3页
本文以中国植物志为研究对象,根据植物分类的特点和植物志检索、鉴定、统计等要求,以索引文件的形式来表示各分类群的特征信息和它们之间的分类关系。设计并实现了中国植物志的数据库模型和信息组织。用计算机来进行植物的检索、鉴定... 本文以中国植物志为研究对象,根据植物分类的特点和植物志检索、鉴定、统计等要求,以索引文件的形式来表示各分类群的特征信息和它们之间的分类关系。设计并实现了中国植物志的数据库模型和信息组织。用计算机来进行植物的检索、鉴定和统计。本课题是中国科学院科学基金资助的课题,已经顺利通过鉴定。 展开更多
关键词 植物志 植物分类 植物志数据库 信息组织
下载PDF
基于非单调推理的领域专家知识库的研究 被引量:2
15
作者 夏幼明 夏幼安 +1 位作者 徐天伟 赵景秀 《计算机科学》 CSCD 北大核心 2001年第9期106-108,共3页
At first,this paper introduces the last results of knowledge presenting and reasoning,basic conception and research methods of nonmonotony. Then,we enlarge ability to express knowledge in semantic network language,and... At first,this paper introduces the last results of knowledge presenting and reasoning,basic conception and research methods of nonmonotony. Then,we enlarge ability to express knowledge in semantic network language,and put forward knowledge presenting way of modal logic. Finally,we provide arithmetic of modal logic reason. 展开更多
关键词 人工智能 非单调推理 知识表示 领域专家知识库
下载PDF
面向对象的ORACLEPRO*C应用软件开发工具 被引量:4
16
作者 李彤 王黎霞 《计算机应用研究》 CSCD 1996年第3期37-39,共3页
OO—HLL是我们设计的一个ORACLEPRO*C应用软件开发工具,它以面向对象和第四代语言面向问题的非过程化方式定义用户需求,生成可嵌入SQL语句到C程序中的PRO*C程序。本文介绍了OO-HLL的基本思想、结构... OO—HLL是我们设计的一个ORACLEPRO*C应用软件开发工具,它以面向对象和第四代语言面向问题的非过程化方式定义用户需求,生成可嵌入SQL语句到C程序中的PRO*C程序。本文介绍了OO-HLL的基本思想、结构、工作流程、类和对象的定义方式,讨论了它的实现技术。 展开更多
关键词 面向对象 软件开发工具 OO-HLL语言 应用程序
下载PDF
实现Internet网多项应用服务功能的综合性工具──Netscape浏览器 被引量:2
17
作者 张艳 胡继普 侯效礼 《计算机应用研究》 CSCD 1996年第6期11-14,共4页
本文介绍了Netscape浏览器作为实现Internet网多项应用服务功能的综合性工具及其实现方法。
关键词 WWW NETSCAPE浏览器 FTP文件 INTERNET网
下载PDF
标记模态归结的推广 被引量:1
18
作者 孙吉贵 刘瑞胜 陈荣 《计算机学报》 EI CSCD 北大核心 1999年第2期113-119,共7页
本文将作者提出的高效的命题模态D逻辑的标记模态归结方法推广到了命题模态逻辑K,K4,D4,T,S4系统,建立了上述命题模态逻辑的标记归结形式系统MRK,MRK4,MRD4,MRT,MRS4.并用转换子句模式的方法,借... 本文将作者提出的高效的命题模态D逻辑的标记模态归结方法推广到了命题模态逻辑K,K4,D4,T,S4系统,建立了上述命题模态逻辑的标记归结形式系统MRK,MRK4,MRD4,MRT,MRS4.并用转换子句模式的方法,借助于标记模态归结对命题模态D逻辑的可靠性结果,证明了标记模态归结系统MRK,MRK4,MRD4,MRT,MRS4分别关于命题模态逻辑K,K4,D4,T,S4的可靠性.进而得到了它们的完备性. 展开更多
关键词 模态逻辑 模态推理 标记模态归结
下载PDF
模态K_4、D_4系统的归结推理 被引量:1
19
作者 孙吉贵 李乔 刘叙华 《软件学报》 EI CSCD 北大核心 1995年第12期742-750,共9页
本文将P.Enjalbert和L.FarinasdelCerro提出的模态归结推理方法推广到命题模态逻辑K4和D4系统,建立了K4逻辑的归结推理RK4;D4逻辑的归结推理RD4,分别证明了RK4和RD4关于K4和D4... 本文将P.Enjalbert和L.FarinasdelCerro提出的模态归结推理方法推广到命题模态逻辑K4和D4系统,建立了K4逻辑的归结推理RK4;D4逻辑的归结推理RD4,分别证明了RK4和RD4关于K4和D4的可靠性与完备性. 展开更多
关键词 模态逻辑 自动推理 归结推理 K4系统 D4系统
下载PDF
模糊命题模态逻辑的Tableau方法 被引量:1
20
作者 刘磊 王强 吕帅 《哈尔滨工程大学学报》 EI CAS CSCD 北大核心 2017年第6期914-920,共7页
为提高模糊命题模态逻辑(fuzzy propositional modal logic,FPML)的推理能力,本文将经典模态逻辑中的Tableau方法推广到FPML中,提出了基于FPML的Tableau规则并证明了其正确性,给出了模糊断言集合的约简策略;在此基础上给出了FPML中的不... 为提高模糊命题模态逻辑(fuzzy propositional modal logic,FPML)的推理能力,本文将经典模态逻辑中的Tableau方法推广到FPML中,提出了基于FPML的Tableau规则并证明了其正确性,给出了模糊断言集合的约简策略;在此基础上给出了FPML中的不一致性和不一致估值的定义。最后给出基于Tableau方法的FPML的一致性检测方法 TFPML和模糊断言集合的不一致估值计算方法 CID,并证明了其正确性。实例分析表明,本文提出的方法是正确有效的。 展开更多
关键词 TABLEAU方法 模态逻辑 模糊命题模态逻辑 不确定推理 一致性检测 模糊断言集合
下载PDF
上一页 1 2 7 下一页 到第
使用帮助 返回顶部