期刊文献+
共找到383篇文章
< 1 2 20 >
每页显示 20 50 100
机械化定理证明研究综述 被引量:7
1
作者 江南 李清安 +2 位作者 汪吕蒙 张晓瞳 何炎祥 《软件学报》 EI CSCD 北大核心 2020年第1期82-112,共31页
随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明... 随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向. 展开更多
关键词 定理证明 证明助手 消解 自然演绎 类型化的λ演算 编程逻辑 求精
下载PDF
基于免疫进化规划的一种柔性神经模糊推理系统 被引量:3
2
作者 付利华 何华灿 《计算机工程与应用》 CSCD 北大核心 2004年第18期19-22,共4页
该文基于泛逻辑学提出一种新颖的柔性神经模糊推理系统,用命题间的广义相关性和广义自相关性去解释系统推理模式的连续可变,以及命题真值的测量误差,以期实现真正的智能控制系统,并采用了将进化规划同生物免疫思想中的浓度机制及多样性... 该文基于泛逻辑学提出一种新颖的柔性神经模糊推理系统,用命题间的广义相关性和广义自相关性去解释系统推理模式的连续可变,以及命题真值的测量误差,以期实现真正的智能控制系统,并采用了将进化规划同生物免疫思想中的浓度机制及多样性保持策略相结合的免疫进化规划学习算法,自适应地学习系统参数。最后通过倒立摆的仿真实验体现了该推理系统的可用性和有效性。 展开更多
关键词 泛逻辑 广义相关性 广义自相关性 免疫进化规划
下载PDF
词计算和语言动力学系统的计算理论框架 被引量:28
3
作者 王飞跃 《模式识别与人工智能》 EI CSCD 北大核心 2001年第4期377-384,共8页
词计算(Computing with Words,简写为CM)是以词或术语(linguistic terms)为对象,而不是以数值为对象的计算方法;而语言动力学系统(Linguistic Dynamic Systems,简写为LDS)就是以词计算为基础,对问题进行动态描述,分析,综合,进而设计,控... 词计算(Computing with Words,简写为CM)是以词或术语(linguistic terms)为对象,而不是以数值为对象的计算方法;而语言动力学系统(Linguistic Dynamic Systems,简写为LDS)就是以词计算为基础,对问题进行动态描述,分析,综合,进而设计,控制和评估的系统。本文通过融合几个不同领域的概念和方法,提出基于词计算的语言动力学系统的计算理论框架,这个框架中的主要概念和方法来源于以下四个方面:1)Kosko关于模糊集的几何表示2)Hsu针对非线性动力学系统的计算所提出的胞映射和分析方法;3)数论数值方法中的最佳格点集和均匀格点集;4)最优控制理论中的动态规划算法,根据这个计算理论框架,我们可以利用常规或传统数值动力学系统中已有的成熟概念和方法,对语言动力学系统进行动力学分析、设计、综合,以及控制和性能评估本文所提出的理论对于模型、目标、控制和反馈主要是以词或文字术语为基础的系统的建模和分析具有重要的应用前景。 展开更多
关键词 词计算 语言动力学系统 模糊逻辑 计算理论 自然语言处理 计算机
原文传递
软件过程建模语言研究 被引量:19
4
作者 柳军飞 唐稚松 《软件学报》 EI CSCD 北大核心 1996年第8期449-457,共9页
本文介绍了软件过程建模的基本概念,提出了对软件过程建模语言的基本要求并简要介绍了几个有代表性的过程建模语言,给出了一个基于时序逻辑的形式化过程建模语言XYZ/PME,该语言是时序逻辑语言XYZ/E的子语言,它支持以角... 本文介绍了软件过程建模的基本概念,提出了对软件过程建模语言的基本要求并简要介绍了几个有代表性的过程建模语言,给出了一个基于时序逻辑的形式化过程建模语言XYZ/PME,该语言是时序逻辑语言XYZ/E的子语言,它支持以角色为中心的逐步求精的过程建模方法,可在统一的形式框架内表示不同抽象级的过程模型.软件过程,软件过程建模,过程建模语言,时序逻辑,程序设计语言. 展开更多
关键词 软件过程 建模 过程建模语言 程序语言
下载PDF
关联图与主动规则集的终止性分析 被引量:15
5
作者 左万利 刘居红 刘淑芬 《软件学报》 EI CSCD 北大核心 2001年第2期276-282,共7页
终止性反映了主动数据库系统良好的行为特性 .目前有关主动规则集终止性分析的主要依据是触发图和活化图 ,其分析结果是保守的 .为表达一个规则的动作可能使另一规则的条件为假的事实 ,引入了惰化图 ( deacti-vation graph) ,并与触发... 终止性反映了主动数据库系统良好的行为特性 .目前有关主动规则集终止性分析的主要依据是触发图和活化图 ,其分析结果是保守的 .为表达一个规则的动作可能使另一规则的条件为假的事实 ,引入了惰化图 ( deacti-vation graph) ,并与触发图和活化图相结合 ,定义了更为一般的关联图 ( relationship graph) .同时 ,给出了基于关联图的主动规则集终止性静态分析算法 ,提高了终止性判定的准确性 . 展开更多
关键词 主动数据库 EAC-规则 终止性 静态分析 关联图 惰化图
下载PDF
Visual Prolog的回溯机制分析 被引量:12
6
作者 雷英杰 王涛 +1 位作者 赵晔 王建勋 《空军工程大学学报(自然科学版)》 CSCD 2004年第5期80-84,共5页
回溯机制是逻辑程序设计的重要设施。回溯本身是一种获得目标所有可能解的良好方法。在考察VisualProlog回溯机制作用原理的基础上,通过若干实例,详细阐述了回溯机制所遵循的4个基本原则,即自顶向下逐层搜索原则、从左到右顺序扫描原则... 回溯机制是逻辑程序设计的重要设施。回溯本身是一种获得目标所有可能解的良好方法。在考察VisualProlog回溯机制作用原理的基础上,通过若干实例,详细阐述了回溯机制所遵循的4个基本原则,即自顶向下逐层搜索原则、从左到右顺序扫描原则、规则匹配原则、事实匹配原则,给出了回溯机制的循环实现方法,深入分析了回溯过程可能发生的各种情况,从而揭示出回溯机制的本质特性和应用机理。结论指出回溯机制具有副作用,需要利用截断机制、失败谓词等对搜索过程进行仔细控制。 展开更多
关键词 VISUAL PROLOG 逻辑程序设计 编程语言 AI 专家系统
下载PDF
项目教学中应用迭代开发方法的研究和实践 被引量:16
7
作者 陈战胜 王廷梅 李明 《计算机教育》 2010年第7期130-133,共4页
本文主要介绍迭代式项目教学法在高职教学中的应用,引入现代软件工程的迭代开发方法,给出迭代项目教学的设计方法和设计原则,并以Java程序设计课程为例详细阐述实施过程,指出在实施过程中应包含的三个步骤和迭代内容,最后说明采用迭代... 本文主要介绍迭代式项目教学法在高职教学中的应用,引入现代软件工程的迭代开发方法,给出迭代项目教学的设计方法和设计原则,并以Java程序设计课程为例详细阐述实施过程,指出在实施过程中应包含的三个步骤和迭代内容,最后说明采用迭代项目教学法对培养学生编程逻辑思维、提升编程兴趣、掌握编程技能产生良好的效果。 展开更多
关键词 迭代 项目教学 教学设计 编程逻辑 JAVA程序设计
下载PDF
归纳逻辑程序设计综述 被引量:3
8
作者 郑磊 贾东 刘椿年 《计算机工程与应用》 CSCD 北大核心 2003年第17期43-46,86,共5页
归纳逻辑程序设计是由机器学习与逻辑程序设计交叉所形成的一个研究领域,是机器学习的前沿研究课题。该文首先从归纳逻辑程序设计的问题背景、类型划分和搜索程序子句三个方面介绍了归纳逻辑程序设计系统的概貌;然后结合实验室的相关研... 归纳逻辑程序设计是由机器学习与逻辑程序设计交叉所形成的一个研究领域,是机器学习的前沿研究课题。该文首先从归纳逻辑程序设计的问题背景、类型划分和搜索程序子句三个方面介绍了归纳逻辑程序设计系统的概貌;然后结合实验室的相关研究工作,回顾了归纳逻辑程序设计研究的发展;之后介绍了归纳逻辑程序设计领域中需要深入研究的若干问题,并提出了新的解决思路;最后是总结,以引起读者对归纳逻辑程序设计领域研究的进一步关注。 展开更多
关键词 机器学习 逻辑程序设计 归纳逻辑程序设计 粗糙—归纳逻辑程序设计 遗传归纳逻辑程序设计 约束归纳逻辑程序设计 关系数据挖掘
下载PDF
汉英机器翻译中描述型复句的关系识别与处理 被引量:12
9
作者 鲁松 宋柔 《软件学报》 EI CSCD 北大核心 2001年第1期83-93,共11页
汉英机器翻译的复句处理不仅要依托于单句的处理 ,而且还要超越单句的辖域 ,深入考察复句内分句之间的内在联系 .其中 ,在汉语描述型复句中存在着大量的无特定语言标记的非并列关系复句 ,为了辨别其中的内在联系 ,实现英语译文的正确生... 汉英机器翻译的复句处理不仅要依托于单句的处理 ,而且还要超越单句的辖域 ,深入考察复句内分句之间的内在联系 .其中 ,在汉语描述型复句中存在着大量的无特定语言标记的非并列关系复句 ,为了辨别其中的内在联系 ,实现英语译文的正确生成 ,针对不同情况 ,给出了完整的关系判定规则 ,并提出采用中心分句动态判定方法来解决部分复句处理规则局部性的问题 ,最后通过实验系统得以验证 . 展开更多
关键词 汉英机器翻译 描述型复句 关系识别 复句处理 信息处理
下载PDF
基于逻辑程序的安全协议验证 被引量:7
10
作者 李梦君 李舟军 陈火旺 《计算机学报》 EI CSCD 北大核心 2004年第10期1361-1368,共8页
安全协议本质上是分布式并发程序 ,可以自然地描述为多个子进程的并发合成系统 .将安全协议对应的并发合成系统抽象为逻辑程序进行消解 ,能够对安全协议无穷多个会话的交叠运行进行验证 .该文提出了安全协议逻辑程序中逻辑规则的一个分... 安全协议本质上是分布式并发程序 ,可以自然地描述为多个子进程的并发合成系统 .将安全协议对应的并发合成系统抽象为逻辑程序进行消解 ,能够对安全协议无穷多个会话的交叠运行进行验证 .该文提出了安全协议逻辑程序中逻辑规则的一个分类方法 ,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法 .逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算 .由于安全协议逻辑程序不动点迭代计算过程不一定终止 ,文中提出了每进行k 1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略 . 展开更多
关键词 安全协议 逻辑程序 不动点 验证策略 验证 互联网络 通信安全
下载PDF
Visual Prolog的搜索控制机制分析 被引量:8
11
作者 雷英杰 王宝树 +1 位作者 赵晔 王涛 《计算机科学》 CSCD 北大核心 2005年第4期52-54,共3页
回溯机制是逻辑程序设计的重要设施。回溯本身是一种获得目标所有可能解的良好方法。然而回溯也有副作用,一是它可能导致Visual Prolog给出多余的答案,而Visua1 Prolog自己不能区分实质上相同的两个解,因此会降低效率;二是尽管一个特殊... 回溯机制是逻辑程序设计的重要设施。回溯本身是一种获得目标所有可能解的良好方法。然而回溯也有副作用,一是它可能导致Visual Prolog给出多余的答案,而Visua1 Prolog自己不能区分实质上相同的两个解,因此会降低效率;二是尽管一个特殊的目标已被满足,但是回溯机制可能还会强迫Visual Prolog 继续寻找另外的解,因此会增加系统开销。在这些情况下,必须仔细控制目标搜索求解的回溯过程。本文在揭示Visual Prolog回溯机制所存在问题的基础上,通过实例,对Visual Prolog的静态截断机制、失败谓词fail与否定谓词not等控制谓词,以及动态截断机制等所构成的完整的目标搜索求解控制机制进行了详细分析,从而揭示出回溯机制和搜索求解控制机制的本质特性及应用机理。 展开更多
关键词 Visual PROLOG 机制分析 逻辑程序设计 目标搜索 控制机制 系统开销 应用机理 本质特性 回溯 副作用 低效率 求解 谓词 截断
下载PDF
多维度数据分级分类安全管理框架 被引量:10
12
作者 刘红 张越今 +1 位作者 赵文霞 杨牧 《信息网络安全》 CSCD 北大核心 2021年第10期48-53,共6页
针对目前数据分级分类安全管理缺乏统一标准和框架,传统的分级分类方法的表达能力有限等情况,文章提出一种利用声明式逻辑编程语言,建立多维度数据分级分类的表达和计算的系统框架,能够实现细粒度的分级分类设定、高效查询和分析。首先... 针对目前数据分级分类安全管理缺乏统一标准和框架,传统的分级分类方法的表达能力有限等情况,文章提出一种利用声明式逻辑编程语言,建立多维度数据分级分类的表达和计算的系统框架,能够实现细粒度的分级分类设定、高效查询和分析。首先在表达能力和复杂度方面,除了支持传统的安全标签,还支持不面向数据记录、带参数、涉及多个数据资源相互作用关系等方式的分级分类,并给出了实例。然后基于分级分类,在同一框架下还能够进行多种数据安全分析和管理。利用纯声明式语言的特性,能够在现有系统上以较小代价实现分级分类安全管理,并允许底层计算框架和存储方式与上层分级分类逻辑的解耦,有利于进行系统优化升级,减小安全机制对系统性能的影响,促进数据分级分类安全管理落地。 展开更多
关键词 数据安全 分级分类 逻辑编程 大数据
下载PDF
Visual Prolog截断机制对回溯的作用机理 被引量:6
13
作者 雷英杰 华继学 +1 位作者 徐彤 狄博 《计算机工程》 EI CAS CSCD 北大核心 2005年第18期183-185,共3页
回溯是一种获得目标所有可能解的良好方法。然而不恰当地使用回溯,可能导致系统效率降低,时空开销增大,因此必须设置相应机制,仔细控制回溯过程。VisualProlog的控制谓词,即失败谓词fail和否定谓词not,与截断机制,包括静态截断机制和动... 回溯是一种获得目标所有可能解的良好方法。然而不恰当地使用回溯,可能导致系统效率降低,时空开销增大,因此必须设置相应机制,仔细控制回溯过程。VisualProlog的控制谓词,即失败谓词fail和否定谓词not,与截断机制,包括静态截断机制和动态截断机制,构成了完整的目标搜索求解控制机制,可以实现对搜索过程的仔细控制,减少不必要的回溯。该文在考察VisualProlog回溯机制和截断机制的基础上,通过实例,对其静态截断机制和动态截断机制进行了详细分析,从而揭示回溯机制和截断机制的本质特性和应用机理。 展开更多
关键词 VISUAL PROLOG 逻辑程序设计 编程语言 专家系统
下载PDF
用Visual Basic6.0设计四通道串口数据采集 被引量:6
14
作者 邓洪声 舒大文 《昆明理工大学学报(理工版)》 2004年第2期57-60,共4页
探讨了串口数据采集在工业中的应用 ,并针对运用VisualBasic 6.0设计四通道串口数据采集做了详细的介绍 .文中详细介绍了串口数据采集中涉及的逻辑电路、串口属性设置及数据采集 。
关键词 VISUALBASIC6.0 四通道 数据采集 串口通信 逻辑电路 程序设计语言
下载PDF
WITNESS环境下基于改进型IDEF3方法的离散事件仿真建模 被引量:5
15
作者 夏守长 奚立峰 +1 位作者 王炬香 胡宗武 《上海交通大学学报》 EI CAS CSCD 北大核心 2004年第6期892-896,共5页
针对WITNESS仿真环境下,复杂离散事件仿真建模过程中出现的大量顺序、并行、同步、冲突及因果依赖等关系,提出采用改进型IDEF3方法进行仿真建模.采用仿真规则与交汇点集成、行为单元与仿真信息数据集成的原则进行建模;同时在IDEF3方法... 针对WITNESS仿真环境下,复杂离散事件仿真建模过程中出现的大量顺序、并行、同步、冲突及因果依赖等关系,提出采用改进型IDEF3方法进行仿真建模.采用仿真规则与交汇点集成、行为单元与仿真信息数据集成的原则进行建模;同时在IDEF3方法的基础上,建立新的行为单元,达到了仿真单元的可重用和可重构性,大大提高了仿真建模的速度,减少了建模难度.最后,给出了在改进型IDEF3方法下进行离散事件仿真的框架,并在仿真软件WITNESS的基础上,通过实例详细描述了建模过程. 展开更多
关键词 改进型IDEF3方法 离散事件 仿真建模
下载PDF
基于逻辑规则的语义缓存查询处理优化技术 被引量:6
16
作者 郝小卫 章陶 李磊 《计算机学报》 EI CSCD 北大核心 2005年第7期1096-1103,共8页
语义缓存在移动计算环境中有着非常广阔的应用前景.查询处理是语义缓存的一个关键问题,但是现有的查询处理算法在时空效率和裁剪结果的复杂度两个方面存在很大的局限性,这在一定程度上限制了语义缓存的实用性.为了克服这些缺陷,作者首... 语义缓存在移动计算环境中有着非常广阔的应用前景.查询处理是语义缓存的一个关键问题,但是现有的查询处理算法在时空效率和裁剪结果的复杂度两个方面存在很大的局限性,这在一定程度上限制了语义缓存的实用性.为了克服这些缺陷,作者首先给出并证明了用于优化查询裁剪的逻辑规则;基于这些规则,给出了剩余查询的裁剪算法;最终给出了只需进行剩余查询裁剪的优化查询处理算法.算法分析从理论上证明了该优化机制的有效性,同时,仿真实验的性能比较也表明该优化方法在提高查询裁剪时空效率和降低剩余查询复杂度等方面都要明显优于没有优化的方法. 展开更多
关键词 语义缓存 查询处理 查询裁减 逻辑规则 优化
下载PDF
溯因推理研究:现状与问题 被引量:6
17
作者 陈荣 姜云飞 林笠 《计算机科学》 CSCD 北大核心 2003年第5期23-25,36,共4页
The notion of abduction was first introduced by the philosopher and logician C. S. Pierce, who claims de-duction, abduction and induction are three different forms of human reasoning. Broadly speaking, abduction is a ... The notion of abduction was first introduced by the philosopher and logician C. S. Pierce, who claims de-duction, abduction and induction are three different forms of human reasoning. Broadly speaking, abduction is a rea-soning process invoked to explain a puzzling observation. The study of logic-based abduction has been the most activeresearch in AI, and there are many results around the subject. This paper surveys the state-of-the-art research andpresents some problems for future work. 展开更多
关键词 人工智能 溯因推理 归纳推理 演绎推理
下载PDF
电压互感器断线原理与应用 被引量:7
18
作者 原治安 《电力自动化设备》 EI CSCD 北大核心 2009年第8期147-150,共4页
详细介绍了美国SEL公司SEL-311C、SEL-749M、SEL-751A电压互感器断线功能,及深圳南瑞公司的ISA-351G馈线保护、ISA-367G线路保护、ISA-353G线路光纤纵差保护、ISA-388G变压器后备保护、ISA-359G电容器保护和ISA-347G电动机保护的电压互... 详细介绍了美国SEL公司SEL-311C、SEL-749M、SEL-751A电压互感器断线功能,及深圳南瑞公司的ISA-351G馈线保护、ISA-367G线路保护、ISA-353G线路光纤纵差保护、ISA-388G变压器后备保护、ISA-359G电容器保护和ISA-347G电动机保护的电压互感器断线功能,分析其逻辑原理,总结优缺点,提出了合理使用电压互感器断线功能的方法。美国SEL公司继电保护装置采用电压互感器断线逻辑判定电压互感器断线,可以灵活运用SEL继电器所具有的逻辑编程功能,编制电压、电流、断路器位置及时间等元件组成的逻辑方程,在电压互感器一相、两相或者三相断线时,进行电压互感器断线判别及进行电压互感器断线闭锁保护的应用。深圳南瑞公司继电保护装置具有母线电压互感器断线逻辑、线路电压互感器断线逻辑,其逻辑中含有电压、电流、断路器位置或时间等元件,在电压互感器一相、两相或者三相断线时,均能够进行电压互感器断线判别及进行电压互感器断线闭锁保护的应用。 展开更多
关键词 电压互感器断线 继电保护 闭锁 断线逻辑 逻辑编程
下载PDF
贝叶斯程序分析
19
作者 张昕 王冠成 +4 位作者 吴宜谦 陈逸凡 李天驰 张羿凡 熊英飞 《电子学报》 EI CAS CSCD 北大核心 2024年第4期1155-1172,共18页
程序分析在软件开发和维护中发挥着关键作用.然而,传统基于逻辑的程序分析方法在处理现代复杂、大规模和动态特性丰富的软件系统时往往效果有限,其根源在于软件系统中的不确定性.研究人员针对具体的程序分析问题提出了一系列新的技术,... 程序分析在软件开发和维护中发挥着关键作用.然而,传统基于逻辑的程序分析方法在处理现代复杂、大规模和动态特性丰富的软件系统时往往效果有限,其根源在于软件系统中的不确定性.研究人员针对具体的程序分析问题提出了一系列新的技术,其特征是在传统逻辑分析的基础上结合概率信息来捕获软件系统中的不确定性.通过总结和抽象这些已有工作,本文提出了贝叶斯程序分析框架,其核心思想是结合程序分析和贝叶斯统计推断,通过建模和更新关于程序的概率分布来推断有关程序行为的信息.贝叶斯程序分析采用概率逻辑编程来同时处理概率信息和逻辑信息,用统一的方式捕获了现有的多项不同工作,也能泛化到程序缺陷定位和差异调试等非传统程序静态分析任务上.本文给出了贝叶斯程序分析框架的定义,展示了该框架在程序分析和相关领域的应用,并展望了未来发展方向. 展开更多
关键词 程序分析 逻辑编程 概率逻辑编程 贝叶斯网络 贝叶斯推断
下载PDF
Semantic Specification and Verification of Data Flow Diagrams 被引量:1
20
作者 刘彤 唐稚松 《Journal of Computer Science & Technology》 SCIE EI CSCD 1991年第1期21-31,共11页
Data Flow Diagram(DFD)has been widely used in Software Engineering as means of require- ment analysis and system specification.However,one defect of DFD approach remains untackled: the lack of formal semantics has bro... Data Flow Diagram(DFD)has been widely used in Software Engineering as means of require- ment analysis and system specification.However,one defect of DFD approach remains untackled: the lack of formal semantics has brought about a lot of problems.In this paper,we model Data Flow Diagram as networks of concurrent processes.With the use of temporal logic language XYZ/E,the formal basis of the semantic specification of DFD can be ensured,and the system prop- erties sach as safety and liveness can be easily characterized.The main part of this paper is devoted to the study of the hierarchical decomposition of semantic specification and its correctness.A verifica- tion methodology is proposed and several examples are analyzed.The implementation of the tools which can support the formal specification,verification and simulation of DFD are also briefly des- cribed. 展开更多
关键词 Computer programming logic programming Computer programming Languages
原文传递
上一页 1 2 20 下一页 到第
使用帮助 返回顶部