模态逻辑D演绎过程的化简规则

发布时间：2020-07-24 12:07

【摘要】：以分析模态逻辑中文字公式的极性为基础，将经典逻辑的Ｄａｖｉｓ－ｐｕｔｎａｍ纯文字化简规则推广到了命题模态逻辑Ｄ系统的自动演绎中，并给出了一些刻划Ｄ逻辑自动演绎特征的化简规则，这些化简规则通过对公式、子公式和公式集的有效性（或不可满足性）的有条件的判断，进行证明过程的剪枝和化简，以提高Ｄ逻辑自动演绎的效率；这些化简规则都是依据公式（集）本身的结构特征，可用于Ｄ逻辑的任意一种推理实现系统，在机器上是容易实现的。

【共引文献】

相关期刊论文 前10条

1 谢康,孙怀民;基于Lakatos证伪方法论的机器发现逻辑[J];北京航空航天大学学报;1992年03期

2 邓安生;刘叙华;;形式模糊命题逻辑推理系统[J];东北师大学报(自然科学版);1989年02期

3 张家锋;徐扬;;格值命题逻辑LP(X)中的语义归结方法[J];辽宁工程技术大学学报(自然科学版);2010年05期

4 张家锋;徐扬;何星星;;格值命题逻辑系统LP(X)的语义归结方法[J];辽宁工程技术大学学报(自然科学版);2011年04期

5 刘富春;;再扩充模糊逻辑中归结方法的有效性[J];广东工业大学学报;2006年01期

6 李凡;归结原理在不精确推理中的应用[J];华中理工大学学报;1992年01期

7 吴尽昭,刘卓军;使用广义奇-超位Ⅱ的一阶定理证明[J];中国科学E辑:技术科学;1996年05期

8 刘叙华,欧阳继红;自动定理证明中RUE-NRF单元输入和锁的演绎[J];吉林大学自然科学学报;1989年02期

9 欧阳丹彤,刘叙华;Horn集上的有向调解法[J];吉林大学自然科学学报;1992年04期

10 刘叙华;广义RUE-NRF归结[J];吉林大学自然科学学报;1993年01期

相关会议论文 前1条

1 于津;刘叙华;;基于不确定、不精确知识的推理系统-UKRS[A];1996年中国智能自动化学术会议论文集（上册）[C];1996年

相关博士学位论文 前4条

1 王体龙;光电侦察中目标快速识别算法研究[D];中国科学院研究生院（长春光学精密机械与物理研究所）;2011年

2 吴瑕;基于扩展规则的定理证明的研究[D];吉林大学;2006年

3 殷明浩;自动推理和智能规划中若干问题研究[D];吉林大学;2008年

4 王建林;基于Isabelle平台的一般拓扑学机械化及自动定理证明研究[D];华东师范大学;2012年

相关硕士学位论文 前4条

1 刘文赫;Horn子句型信念的静态非修正处理方法研究[D];大连海事大学;2011年

2 邹伟松;从归结证明树抽取程序[D];大连理工大学;2002年

3 刘振晗;基于广义归结的程序综合[D];大连理工大学;2005年

4 李晟;命题逻辑公理系统内定理证明的技巧和方法研究[D];燕山大学;2012年

【相似文献】

相关期刊论文 前10条

1 边丽华;闫浩文;刘纪平;褚衍东;;多边形化简前后相似度计算的一种方法[J];测绘科学;2008年06期

2 陈金全;SU(m+n)沔SU(m)×SU(n) ISOSCALAR FACTORS AND S(f_1+f_2)沔S(f_1)×S(f_2) OUTER-PRODUCT ISOSCALAR FACTORS[J];Acta Mathematica Scientia;1985年01期

3 周建涛;叶新铭;;基于组件级化简的语义验证方法在电子商务过程中的应用[J];内蒙古大学学报(自然科学版);2006年02期

4 周建涛;唐旭文;;工作流过程的语义验证方法应用[J];内蒙古大学学报(自然科学版);2006年03期

5 肖林荣,陈偕雄,郑惠群;基于d_j图的逻辑函数布尔偏导数的计算方法[J];浙江大学学报(理学版);2005年05期

6 孙永强;宋国新;;二维数组程序的循环断言确定[J];上海交通大学学报;1983年04期

7 姚勇;王蔼;;矩阵信号流图的化简[J];上海交通大学学报;1985年03期

8 孟令江;;自然推理系统P中的P∧Q■P[J];河北大学学报(自然科学版);2009年03期

9 王士铁;模态逻辑与程序验证[J];厦门大学学报(自然科学版);1985年03期

10 范荣强;;缺省模态逻辑[J];广东技术师范学院学报;1993年04期

相关会议论文 前10条

1 李文江;陈图云;;基于模糊测度的模态逻辑[A];模糊集理论与应用——98年中国模糊数学与模糊系统委员会第九届年会论文选集[C];1998年

2 楚白;;有穷深度的模态逻辑[A];2005年逻辑研究专辑[C];2005年

3 陈国勋;闫家杰;;Fuzzy模态公式的归约[A];中国系统工程学会模糊数学与模糊系统委员会第五届年会论文选集[C];1990年

4 李伟;陈光亭;;若干无人工变量单纯形算法的反例(英文)[A];中国运筹学会第七届学术交流会论文集（下卷）[C];2004年

5 孙希文;;模态逻辑模型的嵌入定理[A];1994年逻辑研究专辑[C];1994年

6 潘天群;;建立在“笛卡尔公理”上的一个怀疑逻辑系统[A];逻辑与认知学术研讨会会议论文集[C];2004年

7 高思存;;一个刻画n叉有限树的模态系统及其应用[A];2005年逻辑研究专辑[C];2005年

8 王真星;吕腾;;本体的描述逻辑到框架表示的转换[A];第二十一届中国数据库学术会议论文集（技术报告篇）[C];2004年

9 马跃峰;;一种形式化的面向对象数据库方法[A];第九届全国数据库学术会议论文集(上)[C];1990年

10 刘大昕;张莉;;数据库自然语言查询接口与类关系代数表达式[A];数据库研究与进展95——第十三届全国数据库学术会议论文集[C];1995年

相关重要报纸文章 前3条

1 许继楠　刘光强;忠诚背后的秘密[N];中国计算机报;2009年

2 陈岸瑛;文字和数字创造的世界[N];中华读书报;2003年

3 陈慕泽;多主体系统中的互知[N];光明日报;2000年

相关博士学位论文 前10条

1 吴瑕;基于扩展规则的定理证明的研究[D];吉林大学;2006年

2 刘全;基于tableau的自动推理研究[D];吉林大学;2004年

3 顾红芳;常识推理中非单调逻辑的研究[D];南京航空航天大学;2001年

4 李文江;基于格蕴涵代数的广义格值模态逻辑及其归结自动推理的研究[D];西南交通大学;2002年

5 史t

本文编号：2768819