基于有向超图的命题逻辑合取范式的约简

来源 :西南交通大学 | 被引量 : 0次 | 上传用户:hldu
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
在知识表示和自动推理领域,命题逻辑是一种极其重要的形式化语言,其中命题逻辑可满足性问题是研究最广泛的核心问题之一,约简命题逻辑公式是由SAT问题衍生的一个子问题。有向超图作为普通有向图的推广,能够恰当地表示大型超网络、数据库系统、命题逻辑等研究课题和研究领域中各元素之间的关系。以有向超图作为工具是众多的命题逻辑公式约简方法中的一种。本文基于命题逻辑和有向超图的相关知识、特别是近期的相关研究工作,主要取得了如下研究结果:  1、针对命题逻辑中一般的合取范式给出了与之一一对应的关联有向超图的定义,给出一种新的超路径表示方式,得到了刻画两个子句和两条超边之间的一些基本关系的等价命题和性质,为进一步利用有向超图寻找并约简具有特定的冗余结构的公式奠定了理论基础。  2、通过定义扩展B-图来表示霍恩公式,得到了其可满足性的若干结论及其约简性质,为进一步约简特定结构的一般公式奠定了基础。  3、将命题逻辑中的冗余对象分为绝对冗余变元、自归入子句、强归结子句这三类。根据两个子句归结的特点又将强归结子句分为具有R1,R2,R3结构的子句。通过研究上述冗余对象和冗余结构,得到了其约简性质,进一步在理论上证明了约简的合理性。  4、针对命题逻辑中五种冗余结构:绝对冗余变元、自归入子句、具有R1,R2,R3结构的强归结子句,提出了相应的约简运算,即弱尾约简、扩展的平行约简、强超边约简、强超路径约简、强连续约简,并辅以实例说明五种约简运算的正确性和有效性。
其他文献
设a是一个次数为d的代数整数,a≠0且非单位根.a=a1,a2,…,ad为a的所有共轭元.ai∈Sθ=(ai∈C:|arg(ai)|≤θ},i=1,2,…,d.P=a0xd+a1xd-1+…+ad=a0∏di=1(x—ai)为a的极小多项式,其中a0=1.
变分不等式是非线性分析理论中的一个重要组成部分,而变分包含是变分不等式的重要推广形式.本文研究了Banach空间中非线性变分包含解的若干问题,主要讨论了非线性变分包含问题
在实线性空间的框架下,我们引进了三种类型的Henig真有效点.利用实线性空间中关于凸集的Hahn-Banach分离定理,我们分别对上述三种类型的Henig真有效点建立了标量化定理.由此,我
本文由四章组成,主要是利用线性系统指数型二分性理论和泛函分析的技巧,以及不动点定理来研究积分微分方程周期解的存在性和稳定性,得到了周期解存在和稳定的充分条件;同时也得到
在研究微分方程稳定性理论中,尤其在探讨微分方程的稳定性,解的估计及有界性的过程中,积分不等式是一强有力的工具近年来,有大批学者从事这方面的理论研究,取得了一系列较好的结果
随着科学技术的不断发展,各种各样的非线性问题已日益引起人们的广泛关注,非线性分析已成为现代数学中的重要研究方向之一.而非线性泛函分析是非线性分析中的一个重要分支,因其
本文研究余代数的表示,全文共分五节. 第一二节为引言与预备知识. 第三节为余模的不可约同态.通过定义余模的不可约同态,几乎可裂序列并探讨其性质,得出余模的不可约同态与极
Boudreault ct.al.在文献[3]中提出了一个索赔额与索赔间隔相依的风险模型,本文将在其基础上进行推广,考虑了阈值分红及借贷问题并得到了如下主要结果:一是Gerber-Shiu期望折