期刊文献+
共找到5篇文章
< 1 >
每页显示 20 50 100
Consistency Property of Finite FC-Normal Logic Programs
1
作者 王以松 张明义 沈榆平 《Journal of Computer Science & Technology》 SCIE EI CSCD 2007年第4期554-561,共8页
Marek's forward-chaining construction is one of the important techniques for investigating the non-monotonic reasoning. By introduction of consistency property over a logic program, they proposed a class of logic pro... Marek's forward-chaining construction is one of the important techniques for investigating the non-monotonic reasoning. By introduction of consistency property over a logic program, they proposed a class of logic programs, FC-normal programs, each of which has at least one stable model. However, it is not clear how to choose one appropriate consistency property for deciding whether or not a logic program is FC-normal. In this paper, we firstly discover that, for any finite logic programⅡ, there exists the least consistency property LCon(Ⅱ) overⅡ, which just depends onⅡitself, such that, Ⅱ is FC-normal if and only ifⅡ is FC-normal with respect to (w.r.t.) LCon(Ⅱ). Actually, in order to determine the FC-normality of a logic program, it is sufficient to check the monotonic closed sets in LCon(Ⅱ) for all non-monotonic rules, that is LFC(Ⅱ). Secondly, we present an algorithm for computing LFC(Ⅱ). Finally, we reveal that the brave reasoning task and cautious reasoning task for FC-normal logic programs are of the same difficulty as that of normal logic programs. 展开更多
关键词 artificial intelligence logic programs stable model consistency property FC-normality
原文传递
约束逻辑程序的良基模型研究 被引量:1
2
作者 常万军 郭祖华 魏昆鹏 《计算机工程》 CAS CSCD 2013年第9期298-302,共5页
在介绍约束逻辑程序的定义、可满足性及其稳定模型等概念的基础上,研究约束逻辑程序的正文字展开方法和约束原子的正文字前缀幂集方法,对展开前后逻辑程序的等价特性进行逻辑证明。分析正规逻辑程序良基模型的构建方法,以求得经展开得... 在介绍约束逻辑程序的定义、可满足性及其稳定模型等概念的基础上,研究约束逻辑程序的正文字展开方法和约束原子的正文字前缀幂集方法,对展开前后逻辑程序的等价特性进行逻辑证明。分析正规逻辑程序良基模型的构建方法,以求得经展开得到的等价正规逻辑程序的最小不动点为切入,给出简单约束逻辑程序交替不动点的良基语义模型。经推理证明,该良基模型是合理的,用该模型的构建方法将约束逻辑程序转化为正规逻辑程序也是可行的。 展开更多
关键词 正规逻辑程序 约束逻辑程序 回答集 最小不动点 良基模型 前缀幂集
在线阅读 下载PDF
时序逻辑程序的模型检测 被引量:4
3
作者 王小兵 段振华 《计算机科学》 CSCD 北大核心 2009年第10期164-167,共4页
时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序p和性质Ф统一表示在投影时序逻辑中... 时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序p和性质Ф统一表示在投影时序逻辑中,模型检测需要判定p→Ф是否有效,可转化为判定p∧Ф是否不可满足,这可以通过构造p∧Ф的正则图加以解决。最后,给出了Framed Tempura程序的模型检测实例。 展开更多
关键词 时序逻辑程序 形式化验证 正则图 模型检测
在线阅读 下载PDF
LFNDIT:从不确定状态变换学习布尔网络
4
作者 黄羿 孔世明 +2 位作者 王以松 张明义 马新强 《计算机科学》 CSCD 北大核心 2020年第11期268-274,共7页
布尔网络是一种重要的基因调控数学模型,从布尔网络的状态变换推断其结构以发现基因之间的调控关系是布尔网络研究中长期关注的重要问题。已有的归纳逻辑程序算法不能从布尔网络的不确定(解释)状态变换学习推断其网络结构。为此,文中提... 布尔网络是一种重要的基因调控数学模型,从布尔网络的状态变换推断其结构以发现基因之间的调控关系是布尔网络研究中长期关注的重要问题。已有的归纳逻辑程序算法不能从布尔网络的不确定(解释)状态变换学习推断其网络结构。为此,文中提出了非确定解释转换学习(Learning From Non-deterministic interpretation Transitions,LFNDIT)算法从布尔网络异步更新语义下的解释变换学习其网络结构。首先将异步更新语义下的不确定解释变换集转换成确定解释变换集,然后利用Inoue等提出的从1步解释转换学习(Learning From 1-step state transition,LF1T)算法计算其对应的正规逻辑程序(布尔网络)。该算法的完备性得到了证明,初步的实验结果表明,该方法能有效地从不确定状态变换计算布尔网络的结构,从而为发现布尔网络的结构提供了新的思路。 展开更多
关键词 归纳逻辑程序 布尔网络 异步布尔网络 正规逻辑程序 LFNDIT算法
在线阅读 下载PDF
良基归纳法在时序逻辑程序不变式验证中的应用 被引量:1
5
作者 杨潇潇 段振华 《计算机科学》 CSCD 北大核心 2009年第6期150-152,共3页
并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义。以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所... 并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义。以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证。提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式,尤其是循环结构的不变量性质。 展开更多
关键词 时序逻辑程序 正则形 良基关系 良基归纳法 不变式证明
在线阅读 下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部