摘要：　　1引言　　一直以来,从逻辑系统到算术系统的转换都依赖于人工的描述,没有自动转换系统.例如,逻辑系统中已有以下信息:某班学生中选修数据结构课程的有50人,选修软件工程课程的有40人,两门课程都选修的有25人,求某课程的平均成绩.解决这样的问题,通常需要在逻辑程序设计语言系统中另外编写程序,执行后才能得到解答.……

摘要：基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。

摘要：需求的变更影响分析过程无论是对于降低系统维护的代价或者是保证系统对变更需求正确的实现都有着至关重要的意义。已有的变更影响分析的研究主要存在两个方面的问题:一方面,当前的有关需求变更影响分析的研究主要侧重于需求到代码之间的变更影响分析,缺乏需求与需求之间的变更影响分析的研究。另一方面,传统的方法大多数是基于需求文档描述做研究,缺乏需求间关系的语义,在作变更影响分析时,会导致大量的变更影响误报,从而忽略了实际的变更影响。为了解决以上这些问题,本文提出了一种基于一阶逻辑的变更影响分析方法。设计一个只包含需求追踪关系信息实体的需求元模型,基于该模型设计一种变更分类方法,并基于一阶逻辑给出需求间关系以及每种变更类型的形式化语义,自动实现需求模型中变更的传播。并通过一个实验来说明本文方法的可行性。

摘要：归纳逻辑程序设计(inductive logic programming,ILP)是以一阶逻辑归纳理论为基础,并以一阶逻辑为表达语言的符号规则学习方法.ILP学得的模型是易于理解的一阶逻辑符号规则,而非难以解释的黑箱模型;在学习中可以相对容易地显式利用以一阶逻辑描述的领域知识;学得模型能对领域中个体间的关系进行建模,而非仅仅对个体的标记进行预测.然而,由于潜在假设空间巨大,进行高效学习有相当的困难.综述了ILP领域的研究情况,从不同一阶逻辑归纳理论的角度对主流的ILP方法做出了梳理.还介绍了近年来ILP基于二阶诱导推理理论的扩展、基于概率的扩展和引入可微构件的扩展.最后,介绍了ILP在实际任务中的代表性应用,探讨了ILP方法目前所遇到的挑战,并对其未来发展进行了展望.

摘要：全国现代逻辑学术讨论会述要邹崇理中国逻辑学会与哈尔滨师范大学、黑龙江省社科联等单位联合举办的现代逻辑学术讨论会于１９９３年８月上旬在哈尔滨召开，来自全国各地的７０多位专家学者参加了会议。会议期间，学者们就符号逻辑、现代归纳逻辑及西方逻辑史诸领域内的学...

摘要：针对一阶逻辑在复杂结构数据环境中存在模式搜索空间庞大和不能发明新谓词的缺点,提出了使用类型化的高阶逻辑知识表示语言Escher去表示各种复杂结构的数据,利用其强类型语法有效地约束知识发现过程中模式的搜索空间和高阶的特点去解决新谓词构造的问题。设计了以Escher为基础的复杂结构数据中的知识发现过程和基于复杂结构数据的聚类算法,并以实验验证了其有效性。

摘要：应用本体论对电子商务知识建模 ,提出电子商务知识描述的分层框架 ,并结合描述逻辑、框架系统设计面向电子商务的知识描述语言 (KDL) .介绍了KDL的语法 ,从一阶逻辑的角度分析KDL的语义特征 ,提供KDL描述到一阶逻辑表达式的映射方法 .最后 ,通过实例证明KDL具有规范的语法、精确的语义和较强的逻辑推理能力 .

摘要：针对民机安全关键系统在正向研发过程中,系统级需求的正确性难以在设计早期全部完成确认的问题,提出一种基于有限谓词追踪的功能需求一致性检查体系。首先,引入一阶逻辑中的谓词追踪,建立系统内部功能需求与交互功能需求形式化规约方法。其次,针对单条、多条需求内容正确性以及需求关系一致性,构建需求一致性检查形式化规约,开展需求自冲突、集冲突与需求关系一致性检验,并生成可解释的检查反例进行需求迭代。最后,以机载平视显示(head-up display,HUD)系统飞行信息符号生成与显示功能为例,验证该方法的正确性与有效性。研究结果表明,基于有限谓词追踪的功能需求一致性检查方法能够提高需求一致性检查效率、降低研发成本,为民机系统级需求确认提供支持。

摘要：数理逻辑是离散数学课程中研究推理的逻辑学科,它为确定一个给出的论证是否有效提供各种法则和技巧,在计算机科学里用来检验程序的正确性,也可以验证定理和推论,同时在计算机模型、计算机程序设计语言、计算机硬件系统等方面有着重要作用。研究数理逻辑在计算机科学领域中的应用,必须从研究数理逻辑的符号化开始讨论、加以分析、验证结论。

摘要：从气象服务分类和等级划分出发,提出了一种基于互联网联盟(W3C)OWL 2标准的气象服务本体化设计思路及其实现方法。在理解气象服务概念的逻辑定义、等级划分的基础上,提出用颜色标尺作为知识的度量,用阶梯函数表达气象服务指标,用一阶逻辑、复合命题逻辑将阶梯函数表达为基于气象因子的逻辑判断。随后,将逻辑分析应用于本体设计,形成分类树,得到气象服务本体知识库。在智能代理作用下,自动站地面气象数据被转化为气象服务知识。该气象服务本体知识库已应用于气象灾害自动化分析,近实时气象服务分析图网站发布,自驾出行气象服务和短信气象服务。