期刊文献+
共找到178篇文章
< 1 2 9 >
每页显示 20 50 100
基于有限谓词追踪的民机系统需求一致性检查方法
1
作者 王鹏 岳舒婷 +1 位作者 张帆 董磊 《系统工程与电子技术》 EI CSCD 北大核心 2024年第1期205-218,共14页
针对民机安全关键系统在正向研发过程中,系统级需求的正确性难以在设计早期全部完成确认的问题,提出一种基于有限谓词追踪的功能需求一致性检查体系。首先,引入一阶逻辑中的谓词追踪,建立系统内部功能需求与交互功能需求形式化规约方法... 针对民机安全关键系统在正向研发过程中,系统级需求的正确性难以在设计早期全部完成确认的问题,提出一种基于有限谓词追踪的功能需求一致性检查体系。首先,引入一阶逻辑中的谓词追踪,建立系统内部功能需求与交互功能需求形式化规约方法。其次,针对单条、多条需求内容正确性以及需求关系一致性,构建需求一致性检查形式化规约,开展需求自冲突、集冲突与需求关系一致性检验,并生成可解释的检查反例进行需求迭代。最后,以机载平视显示(head-up display,HUD)系统飞行信息符号生成与显示功能为例,验证该方法的正确性与有效性。研究结果表明,基于有限谓词追踪的功能需求一致性检查方法能够提高需求一致性检查效率、降低研发成本,为民机系统级需求确认提供支持。 展开更多
关键词 需求一致性 定理证明 功能需求正确性 一阶逻辑 需求冲突
下载PDF
一阶逻辑定理证明器中的无效子句删除策略 被引量:1
2
作者 姜世攀 陈树伟 曾国艳 《计算机应用》 CSCD 北大核心 2024年第3期677-682,共6页
在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的... 在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的精确率,在理论上,基于纯文字规则对子句进行再分类。第一类称为无效子句,该类子句不能通过等词替换与某个子句形成互补对,此类子句应完全删除;第二类为相对无效子句,该类子句无法与当前子句集中的子句形成互补对,但能进行等词替换,此类子句应在参与演绎后综合考虑是否删除。在算法实现中,考虑到子句的消去应是动态的过程,当前消去的子句会影响已判断的子句的无效性,提出一种用于判定子句无效性的递归遍历算法。将上述子句约简规则应用于证明器CSE1.5(Contradiction Separation Extension 1.5)中,以2019—2022的CADE(Conference on Automated DEduction)自动定理证明(ATP)系统竞赛中一阶逻辑问题组为测试对象。在300 s内,应用所提算法的CSE1.5_IC比原始CSE1.5总共多证明了27个问题。在两个版本证明器共同证明的所有FNE(FOF theorems without Equality)测试例中,CSE1.5_IC比CSE1.5平均每个问题多约简了28个子句,平均求解时间减少了7.07 s。实验结果表明,所提无效子句约简算法是一种有效的预处理方式,能够提高一阶逻辑子句集的约简精确率,同时能够提高自动定理证明器的证明能力和缩短证明时间。 展开更多
关键词 自动推理 一阶逻辑 子句删除 纯文字规则 无效子句
下载PDF
策略动态组合优化多元演绎算法及应用
3
作者 郭海林 曹锋 +2 位作者 易见兵 李俊 吴贯锋 《浙江大学学报(理学版)》 CAS CSCD 北大核心 2024年第6期732-739,共8页
一阶逻辑自动定理证明是人工智能领域重要的研究分支,其中子句选择策略对于提升定理证明能力具有重要作用。多元矛盾体分离演绎具有许多良好的演绎特性。为更好地指导多元演绎中的子句选择,提出了一种策略动态组合优化多元演绎方法,通... 一阶逻辑自动定理证明是人工智能领域重要的研究分支,其中子句选择策略对于提升定理证明能力具有重要作用。多元矛盾体分离演绎具有许多良好的演绎特性。为更好地指导多元演绎中的子句选择,提出了一种策略动态组合优化多元演绎方法,通过将子句文字数大小和函数项深度进行动态组合并迭代优化,在充分发掘现有多元演绎启发式策略的同时,提升策略应对不同问题的自适应性,实现多元演绎中的子句高效选择。基于该方法给出了相应的算法实现,根据不同问题的演绎过程动态调整子句的选择策略,提升了多元演绎的定理证明能力。同时,将该算法应用于国际先进的证明器Eprover 2.6,形成了改进的证明器SDCO_E,进一步通过2组实验评估SDCO_E的性能。实验1用2021—2023年国际一阶逻辑自动定理证明器竞赛组的共1500个问题进行测试,结果表明,SDCO_E比Eprover 2.6多证明了35个问题,证明定理总数增加了3.06%;实验2用TPTP库中难度系数为1的问题进行测试,结果表明,SDCO_E能证明其他证明器无法证明的6个数论与集合论领域的问题。实验结果表明,策略动态组合优化多元演绎算法能有效应用于一阶逻辑自动定理证明。 展开更多
关键词 一阶逻辑 定理证明 人工智能 多元演绎 组合优化
下载PDF
面向前提选择的新型图约简表示与图神经网络模型
4
作者 兰咏琪 何星星 +1 位作者 李莹芳 李天瑞 《计算机科学》 CSCD 北大核心 2024年第5期193-199,共7页
自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表... 自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型,充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度。首先,将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图;其次,利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新,随后使用注意力机制为图上的节点分配权重,进而调整图节点嵌入信息;最后,将前提图向量和猜想图向量拼接并输入二元分类器中实现前提分类。实验结果表明,所提方法在MPTP数据集和CNF数据集上的准确率分别达到了88.61%和84.74%,超越现有最优的前提选择方法。 展开更多
关键词 图神经网络 前提选择 注意力机制 一阶逻辑公式 图约简表示方法
下载PDF
可满足性模理论综述
5
作者 唐傲 王晓峰 何飞 《计算机工程与科学》 CSCD 北大核心 2024年第3期400-415,共16页
可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广... 可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。 展开更多
关键词 一阶逻辑 可满足性模理论 Lazy方法 DPLL(T) SMT求解器 #SMT
下载PDF
一阶逻辑中基于treelet图神经网络的前提选择
6
作者 马雪 何星星 +1 位作者 兰咏琪 李莹芳 《计算机工程与科学》 CSCD 北大核心 2024年第2期374-380,共7页
前提选择是解决自动定理证明器面对大规模问题时性能降低的有效方法。当前面向一阶逻辑中前提选择的主流图神经网络忽略了逻辑公式图内部的节点顺序信息。针对此问题,将一种面向高阶逻辑公式的保序方法拓展到一阶逻辑中,并提出了一种基... 前提选择是解决自动定理证明器面对大规模问题时性能降低的有效方法。当前面向一阶逻辑中前提选择的主流图神经网络忽略了逻辑公式图内部的节点顺序信息。针对此问题,将一种面向高阶逻辑公式的保序方法拓展到一阶逻辑中,并提出了一种基于treelet的图神经网络模型。该模型在信息聚合时一部分聚合中心节点的父、子节点信息,另一部分聚合节点顺序信息。实验分析表明:基于treelet的图神经网络模型在前提选择任务中比最优的主流图神经网络模型的分类准确率提高了约2%。 展开更多
关键词 一阶逻辑公式 图神经网络 前提选择 二元分类
下载PDF
基于一阶谓词逻辑的结构设计规范表示方法
7
作者 张吉松 于泽涵 赵丽华 《土木与环境工程学报(中英文)》 CSCD 北大核心 2024年第1期254-262,共9页
目前,基于BIM模型的合规性审查采用人工方式,工作量繁重且自动化程度低,开展自动合规性审查研究具有重要意义。在结构设计领域能够有效支撑规范知识表示与推理并支持设计审查自动化的设计规范表达方法有待开发。基于一阶谓词逻辑,通过... 目前,基于BIM模型的合规性审查采用人工方式,工作量繁重且自动化程度低,开展自动合规性审查研究具有重要意义。在结构设计领域能够有效支撑规范知识表示与推理并支持设计审查自动化的设计规范表达方法有待开发。基于一阶谓词逻辑,通过转译《混凝土结构设计规范》中的设计条款,提出一种结构设计规范规则表达和推理方法。该方法可实现将半结构化设计规范条款转换为结构化知识并支持灵活查询与推理,通过“谓词定义”和“函数定义”转译设计规范中语言类、表格类和计算公式类设计条款,提出两种规范条款谓词定义方式。对于语言模糊类、表后注释类和条款补充类的设计条款给出转译解决方案。提出的方法有效地解决了传统一阶谓词对于结构设计条款表示不充分和不精确的问题,进而为设计规范的计算机表达提供一种参考方法。 展开更多
关键词 结构设计规范 知识表示 一阶谓词逻辑 合规性审查 人工智能
下载PDF
DEBRA: On the Unsupervised Learning of Concept Hierarchies from (Literary) Text
8
作者 Peter J. Worth Domagoj Doresic 《International Journal of Intelligence Science》 2023年第4期81-130,共50页
With this work, we introduce a novel method for the unsupervised learning of conceptual hierarchies, or concept maps as they are sometimes called, which is aimed specifically for use with literary texts, as such disti... With this work, we introduce a novel method for the unsupervised learning of conceptual hierarchies, or concept maps as they are sometimes called, which is aimed specifically for use with literary texts, as such distinguishing itself from the majority of research literature on the topic which is primarily focused on building ontologies from a vast array of different types of data sources, both structured and unstructured, to support various forms of AI, in particular, the Semantic Web as envisioned by Tim Berners-Lee. We first elaborate on mutually informing disciplines of philosophy and computer science, or more specifically the relationship between metaphysics, epistemology, ontology, computing and AI, followed by a technically in-depth discussion of DEBRA, our dependency tree based concept hierarchy constructor, which as its name alludes to, constructs a conceptual map in the form of a directed graph which illustrates the concepts, their respective relations, and the implied ontological structure of the concepts as encoded in the text, decoded with standard Python NLP libraries such as spaCy and NLTK. With this work we hope to both augment the Knowledge Representation literature with opportunities for intellectual advancement in AI with more intuitive, less analytical, and well-known forms of knowledge representation from the cognitive science community, as well as open up new areas of research between Computer Science and the Humanities with respect to the application of the latest in NLP tools and techniques upon literature of cultural significance, shedding light on existing methods of computation with respect to documents in semantic space that effectively allows for, at the very least, the comparison and evolution of texts through time, using vector space math. 展开更多
关键词 Ontology Learning Ontology Engineering Concept Hierarchies Concept Mapping Concept Maps Artificial Intelligence PHILOSOPHY Natural Language Processing Knowledge Representation Knowledge Representation and Reasoning Machine Learning Natural Language Processing NLP Computer Science Theoretical Computer Science EPISTEMOLOGY METAPHYSICS PHILOSOPHY logic Computing Ontology first order logic Predicate Calculus
下载PDF
基于大规模语言模型的知识图谱可微规则抽取 被引量:3
9
作者 潘雨黛 张玲玲 +3 位作者 蔡忠闽 赵天哲 魏笔凡 刘均 《计算机科学与探索》 CSCD 北大核心 2023年第10期2403-2412,共10页
知识图谱上的推理是预测不完整三元组中缺失的实体或关系,对结构化知识进行补全,并用于不同下游任务的过程。不同于被普遍研究的黑盒方法,如基于表示学习的推理方法,基于规则抽取的推理方法通过从知识图谱中泛化出一阶逻辑规则,实现一... 知识图谱上的推理是预测不完整三元组中缺失的实体或关系,对结构化知识进行补全,并用于不同下游任务的过程。不同于被普遍研究的黑盒方法,如基于表示学习的推理方法,基于规则抽取的推理方法通过从知识图谱中泛化出一阶逻辑规则,实现一种可解释的推理范式。为解决离散的符号空间与连续的嵌入空间之间的鸿沟,提出一种基于大规模预训练语言模型的知识图谱可微规则抽取方法DRaM,将离散的一阶逻辑规则与连续的向量空间进行融合。针对规则中的原子公式顺序对推理过程产生的影响,通过引入大规模预训练语言模型对推理过程进行编码来解决。融合一阶逻辑规则的可微推理方法DRaM,在三个知识图谱数据集Family、Kinship和UMLS上进行的链接预测任务获得了较好的结果,尤其针对链接预测指标Hits@10,DRaM获得了最佳的推理结果。实验结果表明,DRaM能够有效地解决知识图谱上可微推理存在的问题,并且可以从推理过程中抽取带有置信度的一阶逻辑规则。DRaM不仅通过一阶逻辑规则增强了推理效果,同时增强了方法的可解释性。 展开更多
关键词 知识图谱上的推理 一阶逻辑规则 大规模语言模型(LLM) 可解释推理
下载PDF
基于子句活跃度和复杂度的多元动态演绎算法及应用 被引量:1
10
作者 林玲瑜 曹锋 +3 位作者 易见兵 方旺盛 李俊 吴贯锋 《计算机工程与科学》 CSCD 北大核心 2023年第12期2256-2264,共9页
一阶逻辑自动定理证明是知识表示与自动推理领域重要的研究内容,如何有效选取子句参与演绎是提升自动推理能力和效率的研究热点。基于多元动态演绎良好的演绎特性,通过分析子句的变元项性质和函数项结构,提出了一种子句活跃度和复杂度... 一阶逻辑自动定理证明是知识表示与自动推理领域重要的研究内容,如何有效选取子句参与演绎是提升自动推理能力和效率的研究热点。基于多元动态演绎良好的演绎特性,通过分析子句的变元项性质和函数项结构,提出了一种子句活跃度和复杂度的度量与计算方法,能很好地对不同项结构的子句进行有效评估;基于该子句评估方法,提出了一种子句充分协同演绎的多元动态演绎算法,能有效优化多元演绎搜索路径。将该多元动态演绎算法应用于国际顶尖证明器Eprover 2.6中,以2021年国际自动推理FOF组竞赛例为测试对象,在标准的300 s测试时间内,加入了多元动态演绎算法的Eprover 2.6相比原始Eprover 2.6多证明定理4个,在证明定理总数相同的条件下,平均证明时间减少了1.12 s;能证明Eprover 2.6未证明定理16个,占未证明定理总数的15.1%。实验结果表明,该多元动态演绎算法是一种有效的推理方法,能在一定程度上提升自动定理的证明能力和时间效率。 展开更多
关键词 一阶逻辑 定理证明 自动推理 多元动态演绎 子句评估
下载PDF
针对教学场景的ZFC集合论Coq形式化 被引量:1
11
作者 万新熠 徐轲 曹钦翔 《软件学报》 EI CSCD 北大核心 2023年第8期3549-3573,共25页
离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助... 离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果. 展开更多
关键词 COQ ZFC公理集合论 一阶逻辑
下载PDF
基于多引擎并行协作的SCADE模型检测
12
作者 方雨瑶 张聪 《计算机技术与发展》 2023年第11期86-90,共5页
SCADE语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用。已有的SCADE同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题。为了解决现有的问题,该文提... SCADE语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用。已有的SCADE同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题。为了解决现有的问题,该文提出了多引擎并行协作的方法,通过并行执行BMC引擎、归纳法引擎和程序抽象引擎三个模型检测引擎来实现对SCADE同步语言程序验证的协作,其中程序抽象引擎通过反例引导的抽象精化方法解决了大型复杂程序验证效率低下的问题。实现了一款针对SCADE同步语言程序的模型检测工具PSMC,该工具采用多引擎并行协作方法来提升SCADE同步语言程序模型检测的效率。手动构造了887个SCADE同步语言程序用于对PSMC进行实验验证,结果表明提出的优化方法可以有效地对SCADE同步语言程序进行自动的验证,并且可以提升模型检测的验证效率(约31%)。 展开更多
关键词 同步语言 形式化验证 一阶逻辑 反应系统 可满足性模理论
下载PDF
基于符号权重的一阶逻辑前提选择方法
13
作者 刘清华 李瑞杰 +1 位作者 朱绪胜 陈代鑫 《西南交通大学学报》 EI CSCD 北大核心 2023年第3期704-710,共7页
为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同... 为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同时,研究自适应相关度边界,用于判断前提与给定的结论是否相关;最后,在自动定理证明器中交互地结合前提选择和自动推理两个过程,可在充分选择相关前提的情况下及时停止前提选择过程.实验结果表明:在最优情况下,新提出的前提选择方法能够把参与证明的平均前提数量从1 876个降低到174个;与广泛使用的前提选择方法 E-SInE和Vampire-SInE相比,使用新方法能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率. 展开更多
关键词 前提选择 自动定理证明 一阶逻辑
下载PDF
一阶逻辑命题符号化的研究
14
作者 方冬云 曾宪芾 《榆林学院学报》 2023年第5期57-60,共4页
一阶谓词逻辑作为一种重要的知识表示方法,有着强大的陈述表达能力,能够将思维活动准确的表达出来,而一阶逻辑命题符号化是一阶谓词逻辑的基础,把自然语言用离散数学的相关符号转化为谓词公式。文章着重分析自然语言含有三个或三个以上... 一阶谓词逻辑作为一种重要的知识表示方法,有着强大的陈述表达能力,能够将思维活动准确的表达出来,而一阶逻辑命题符号化是一阶谓词逻辑的基础,把自然语言用离散数学的相关符号转化为谓词公式。文章着重分析自然语言含有三个或三个以上谓词的命题符号化,将每句自然语言分解成多个复合的主谓语,按照“”量词与“→”联结词搭配,“”量词与“∧”联结词搭配的规则进行符号化。通过一阶逻辑命题符号化,利用一阶逻辑等值式及推理规则能高效率处理和解决自然语言领域的相关问题。 展开更多
关键词 一阶逻辑 命题符号化 一阶逻辑等值式
下载PDF
乔姆斯基的形式语言理论与计算机程序的电路控制
15
作者 陈锐 《西部学刊》 2023年第21期156-160,共5页
一阶谓词逻辑是语言学数学化的标准形式,具有公理递归演绎特性;乔姆斯基的形式语言理论和计算机程序语言都具备了一阶谓词逻辑的公理递归特性;计算机语言与乔姆斯基语言学具有完全的逻辑等价性,这使得人工智能处理人类语言成为可能;人... 一阶谓词逻辑是语言学数学化的标准形式,具有公理递归演绎特性;乔姆斯基的形式语言理论和计算机程序语言都具备了一阶谓词逻辑的公理递归特性;计算机语言与乔姆斯基语言学具有完全的逻辑等价性,这使得人工智能处理人类语言成为可能;人类语言最终可以还原为电路中高电压与低电压的有序变化,深刻地证明了物质与意识的辩证统一规律。 展开更多
关键词 一阶谓词逻辑 公理体系 递归 计算机程序语言 乔姆斯基 辩证统一
下载PDF
一阶逻辑vs组合范畴语法:公式、目标与表达力
16
作者 姚从军 林延廷 《贵州工程应用技术学院学报》 2023年第1期51-58,共8页
一阶逻辑和组合范畴语法都是追逐“莱布尼茨之梦”的产物。一阶逻辑独立于自然语言,从人工语言出发,依据公式形成规则,生成逻辑公式;组合范畴语法实现了自然语言表达式的句法和语义的并行推演,伴随句法组合,自动生成相应的语义表达式。... 一阶逻辑和组合范畴语法都是追逐“莱布尼茨之梦”的产物。一阶逻辑独立于自然语言,从人工语言出发,依据公式形成规则,生成逻辑公式;组合范畴语法实现了自然语言表达式的句法和语义的并行推演,伴随句法组合,自动生成相应的语义表达式。一阶逻辑以找出有效的推理模式为目标,关注系统本身的可靠性和完全性;组合范畴语法旨在用形式化的方法判断语句是否合语法和给出语言表达式的形式语义,关注计算机对自然语言的理解和处理。一阶逻辑对自然语言的抽象化程度非常高,舍弃了自然语言的内涵意义;组合范畴语法立足自然语言,全面、细致地刻画自然语言的句法和语义。 展开更多
关键词 一阶逻辑 组合范畴语法 合式公式 有效推理 自然语言处理
下载PDF
On decidability and model checking for a first order modal logic for value-passing processes
17
作者 薛锐 林惠民 《Science in China(Series F)》 2003年第1期45-59,共15页
A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown... A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained. 展开更多
关键词 first order modal logic DECIDABILITY model checking value-passing processes.
原文传递
The Expressibility of First Order Dynamic Logic
18
作者 付斌 李琼章 《Journal of Computer Science & Technology》 SCIE EI CSCD 1992年第3期268-273,共6页
This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG ... This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG K_1 K_2 … RF, such that L (RG)<L (K_1)<L (K_2) < … < L (RF), where RG, RF are regular program class and finitely generated recursively enumerable program class respectively, and L (K) is the first order dynamic logic of program class K. 展开更多
关键词 CASE The Expressibility of first order Dynamic logic
原文传递
COMBINATORY LOGIC AS THE FIRST-ORDER MATHEMATICAL THEORY
19
作者 江明德 文蕙 《Chinese Science Bulletin》 SCIE EI CAS 1989年第24期2079-2083,共5页
I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself o... I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself of the functional and logic paradigms. The purpose of this note, proceeding from the algebraic oersoective, is to formulize the first-order mathematical 展开更多
关键词 combinatory logic PREDICATE CALCULUS first-order mathemtical theory.
下载PDF
使用本体和SWRL验证作战计划的方法 被引量:12
20
作者 钱猛 刘忠 +1 位作者 都业宏 姚莉 《计算机工程与应用》 CSCD 北大核心 2009年第8期208-212,245,共6页
计划验证是计划编制过程的重要环节。从知识管理的角度,在已有计划表示和计划推理相关研究的基础上,提出了一种基于本体和规则的计划验证方法框架,通过对计划知识进行基于本体的表示、基于描述逻辑、一阶谓词逻辑的规则知识抽取和计划推... 计划验证是计划编制过程的重要环节。从知识管理的角度,在已有计划表示和计划推理相关研究的基础上,提出了一种基于本体和规则的计划验证方法框架,通过对计划知识进行基于本体的表示、基于描述逻辑、一阶谓词逻辑的规则知识抽取和计划推理,以实现对计划的验证。并以某排雷作战计划的验证为例进行了实验。实验表明,该方法实现了对专家知识的扩展,提高了作战计划正确性检验的效率。 展开更多
关键词 本体 规则 推理 作战计划验证 WEB本体语言 语义网规则语言 一阶逻辑
下载PDF
上一页 1 2 9 下一页 到第
使用帮助 返回顶部