刘全, 孙吉贵, 于万钧[1]2005年在《基于tableau的自动推理技术综述》文中研究表明tableau方法是一种接近于逻辑系统表示的自动推理方法,由于其直观性和通用性,易于计算机实现,成为目前最普及的自动推理方法之一。在提高系统效率方面,主要在相关技术和策略、理论和方法等方面进行了分析,并展望了未来的研究方向。
刘全[2]2004年在《基于tableau的自动推理研究》文中提出自动定理证明的历史几乎与计算机科学的历史一样长，计算机科学中的尖端领域——人工智能的研究也是从自动定理证明开始的。自动推理作为自动定理证明的扩展是人工智能研究的基础工作，许多重要的人工智能系统，都是以推理系统为其核心部分，所以自动推理的研究，将对人工智能的其它分枝产生深远的影响，它所提出的推理方法已被应用于人工智能的各个领域。 语义tableau方法由Beth(1959)、Hintikka(1955)年提出，而后由人工智能研究者引入到自动定理证明中，tableau方法的实质是将语义结构中的二元关系显式地表现出来。换句话说，就是通过引入相应的谓词，将二元关系的性质用逻辑公式来表示。对于不同的逻辑系统，所使用的tableau规则是相同的，只是对公式构造集进行扩展，使之更接近相应的逻辑系统。由于tableau方法具有较强的通用性和直观性，从二十世纪六十年代开始，引起了以Smullyan、Fitting为代表的计算机科学家的兴趣，同归结一样，被认为是重要的自动推理方法之一。特别是近十年来，引起了更广泛的关注，许多人在寻求各种各样的tableau方法，以求提高效率和易于计算机实现。本论文在tableau方法基础上，研究工作可以分为以下四部分： 第一部分，关于经典逻辑tableau方法研究。 (1)对于量词规则，由于γ-规则替换的任意性，可导致在同一tableau证明中，γ-规则被多次使用，使得tableau结构中出现多个自由变量。另外，δ-规则要求被Skolem化的函数符号是新的，且函数中包含分枝中出现的所有自由变量。显然。由于γ—规则的不确定性以及δ—规则的限制，可使一个简单的证明变得很复杂，延迟了tableau的封闭时间。 在文献[49]中。对δ—规则进行了改进，称δ~+—规则。但对tableau多次出现的自由变量的情况结果仍不太令人满意。在此基础上，对δ~+—规则进行了进一步的改进，称为δ~(++)—规则，并进行了有效性和完备性证明，将δ~(++)—规则应用到TableauTAP系统中，结果表明，改进后的系统对δ公式在实现推理空间上有较大的改进。 (2)在tableau实现时，对γ规则应用次数的限制致关重要，限制次数直接影响tableau的推理效率。我们给出识别γ公式方法，提出了含γ公式的tableau推理的改进策略，并进行了理论证明和系统实现，该系统与leanTAP软件包进行了对比实验，通过对Pelletier问题的20个实例分析，可以看出，γ公式不再需要实例化，大大缩短了tableau的证明过吉林大学博士学位论文程，减少了搜索空间，提高了推理效率. 第二部分，关于多值逻辑tabl。au方法研究. (3)含有量词的一阶多值tableau方法具有统一的扩展规则，并由Zabel等人给出了可靠性和完备性的证明.但由于扩展后的分枝随着真值数目的增加而呈指数的增加，因而影响了机器推理执行的效率.我们提出了布尔剪枝方法，将带符号的公式与集合的上集/下集联系起来，使含量词的一阶多值逻辑公式的扩展规则大大简化.进一步，通过对布尔剪枝方法的分析，建立了一类特殊一阶多值逻辑正则公式的更为简洁的tableau推理方法，该方法使得含量词的一阶多值逻辑tableau推理类同于经典逻辑tableau方法. (4)我们将经典逻辑中的结构保留子句转换方法应用到带符号的多值公式中，产生输入规模是线性的范式.并引入极性的概念，减少冗余子句的产生.利用多值子句tableau方法进行证明，并对适合于经典子句的包含删除、分解子因子等策略修改后，应用到多值子句tableau，使其推理效率大大提高. 第叁部分，关于含等词tableau方法研究. (5)本文在增添扩展规则的tableau方法的基础上提出了一种新的含等词tableau方法—等式合一方法，并证明了其可靠性和完备性.在该方法中，将tableau分成两个阶段，等词单独处理，通过提取等式合一问题并求解解替换封闭tableau，这样进一步限制了tableau的搜索空间，提高了tableau的推理效率.同时，为了研究等式合一方法的有效性，在解替换求解方面，提出了提取不等式析取，并在启发式的帮助下计算等价类的方法.通过实例分析，与Fi tting和Jeffrey方法进行比较，结果表明，等式合一方法优于其它方法. 第四部分，基于tab 1 eau的定理机器证明系统TableauTAP. (6)我们使用SW工一PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP，并证明了其正确性.该系统可以证明不含等词的经典逻辑公式和多值逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展.应用该系统对TPTP的400个逻辑问题进行证明，实验结果表明，Tab 1 eauTAP在时间和空间效率上都是比较高的.
李娇[3]2012年在《基于tableau的数据记录匹配及一致性研究》文中研究指明数据质量已被公认为是数据管理的首要问题之一。针对数据质量管理领域的数据记录不匹配及不一致问题,本文分别从记录匹配检测及不一致修复两个角度出发,提出了基于CON模型的记录匹配方法和基于tableau的自动检测及修复不一致数据库方法。同时,在所提理论的基础上,以eclipse为实验开发平台,将上述算法应用到实验中,实验结果表明,这些方法对于验证数据记录匹配及修复不一致数据库是正确的及有效的。本文的主要研究成果概括为以下叁个方面：(1)提出一种基于局部CON模型的记录匹配方法。该方法利用关联规则发现算法挖掘匹配依赖,将匹配依赖和数据实例同时作为改进型tableau的输入,检测匹配得出结果。理论分析和实验结果表明该方法能快速识别出分布式记录匹配情况,且不需要人工参与,效率有非常明显的提高。(2)以不一致作为CFDs的违反情况,提出一种自动检测及修复不一致数据库的BCFDAR算法,并从理论上证明了算法是可终止的。实验结果表明,该方法能有效地修复不一致数据库,而且CFDs体现出比传统的FDs更高的准确性,并加入优化算法,使得检测修复过程更加高效。(3)利用分支封闭值修复数据库方法,结合tableau分析法的开放和封闭推理标准,以开放公式树TP(IC∪r)(?)分支为基础,为公式树TP(IC∪r)中的每个结点引入一个结点封闭值,通过计算该值来选择分支进行开放修复,并对该过程进行了逻辑证明。最后,对于一致性应答结果的逻辑特征给予了证明。
刘全, 伏玉琛, 孙吉贵, 崔志明, 龚声蓉[4]2007年在《一种基于集合符号的自动推理扩展方法》文中认为在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.
郭远华[5]2009年在《若干逻辑自动推理方法研究》文中研究指明自动定理证明(Automated Theorem Proving)或者机器定理证明(MechanicalTheorem Proving)是通过计算机实现定理证明.二十世纪五十年代以来自动定理证明一直是计算机科学的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用.部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题,检查子句集的满足式映射中的阻塞是该方法的关键.论文提出的子句搜索方法在判定子句集可满足性的同时给出了一个模型从而得到满足式映射.格值逻辑的不完全可比性便于描述人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立,目前对LP(X)系统的自动推理研究主要是归结方法,论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程.归结方法、语义表方法、相继式方法是定理证明中的常用方法,但是重点在于判定而不是演绎,论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现,生成了类似于手工证明的可读证明.具体而言论文的工作包括以下几方面:(1)提出了子句搜索方法判定命题子句集的可满足性并给出可满足子句集的一个模型.子句搜索方法通过查找到子句集Φ不可扩展的子句C来判定Φ的可满足性.结合部分实例化方法将子句搜索方法提升至一阶,分离了谓词公式的结构和变量,从而提高合一算法的效率并节省了存贮空间.用正整数代表原子,负整数代表负文字,简化了算法实现.(2)提出了格值命题逻辑系统LP(X)的tableau方法,语义表中的公式都是受限蕴涵公式.通过引入Bound~s(X)、Bound_s(X)和极大相容集证明了其正确性和完备性.对于真值域可直积分解的系统LP(X),讨论了其格直积分解证明.(3)提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生了类似于手工证明的演绎序列.将公式转化为二叉树的形式存贮于动态数组中减小了公式冗余,用数组下标代表公式简化了实现.(4)提出了应用于自然推理方法的回溯方法.先从假设集出发构建证明树,再从树根节点逐层推导各公式的属性,实现了相干自然推理系统NR的类似手工证明的自然推理方法证明.综上所述,论文提出了判定子句集可满足性的子句搜索方法并将其提升至一阶,提出了格值命题逻辑系统LP(X)的tableau方法,提出了后推试探方法和回溯方法并实现了相干命题逻辑系统R的可读证明,在理论和应用方面都有积极意义.
王炜程[6]2009年在《Tableau基础理论及应用研究》文中进行了进一步梳理自动定理证明的扩展之一:自动推理,是人工智能研究的基础工作。许多重要的人工智能系统,都是以推理系统为其核心部分,所以自动推理的研究,将对人工智能的其它分枝产生深远的影响,它所提出的推理方法已被应用于人工智能的各个领域。其中的语义tableau方法是由Beth(1959)、Hintikka(1955)提出,而后引入到自动定理证明中。它对于不同的逻辑系统,所使用的tableau规则是相同的,只是对公式构造集进行扩展,使之更接近相应的逻辑系统。由于tableau方法具有较强的通用性和直观性,从二十世纪六十年代开始,引起了以Smullyan、Fitting为代表的计算机科学家的兴趣,同归结一样,被认为是重要的自动推理方法之一。特别是近十年来,引起了更广泛的关注,许多人在寻求各种各样的tableau方法。本文在研究tableau理论的基础上,主要在命题和一阶逻辑中做了以下五个方面的研究:1.在基本逻辑表示方式的基础上,重点研究了命题和一阶逻辑的范式表示,通过采用析取式重写等方法,得到了在一阶逻辑下,将任意一阶公式转化为析取范式的方法,并利用Prolog语言进行了实现。2.在逻辑语义的基础上,研究了tableau推理方法(包括命题及一阶),分析原有命题逻辑下实现算法在效率上的不足,对其进行了改进,并进行了有效性和完备性的证明。同样也针对一阶逻辑下的自动推演算法,通过应用与范式转换中相类似的预处理方式进行修改,以简化后期推演程序,提高效率。3.在对基本tableau方法扩展的基础上,研究了含等词的tableau方法。4.在tableau基本理论和方法的基础上,将tableau应用于数据库修正中,解决了此领域中传统修正方法存在的资源消耗大、信息易丢失等问题。5.采用Prolog语言对上述部分理论和方法进行了实现,并根据Prolog语言的特点进行了优化。
高华[7]2015年在《基于Tableau的定理证明器的优化技术研究》文中提出语义Tableau是一种具有较强直观性和适用性的推理方法.自该方法问世以来,一直吸引着大量人工智能研究者.基于Prolog语言,M.C.Fitting利用语义Tableau方法提出了一种一阶逻辑自动定理证明器.众所周知,系统的实现效率问题一直是人工智能界的一个热点问题.M.C.Fitting给出的定理证明器虽然比较容易理解,但是在具体应用过程中却存在着一定的效率问题,论文便是针对这一问题展开了具体的研究.具体的研究内容如下:1论文首先给出了一阶逻辑语言的项、公式、子句等有关的概念,然后在此基础上研究了一阶逻辑语言理论及其模型系统,并重点探讨了Herbrand模型.2论文介绍语义Tableau方法的理论和实现.首先描述了Tableau方法的概念与其在实际应用过程中的语义Tableau扩展规则,并完成了该方法的可靠性和完备性的证明,重点介绍了在证明完备性过程中所要用到的模型存在定理;其次给出了实现该系统的算法与在Prolog语言下的代码.3通过对M.C.Fitting给出的定理证明器中存在的效率问题进行分析研究,提出了相关的改进,并给出了改进后的算法以及该算法可终止性和正确性的证明.最后进行了相应的对比实验,结果表明:优化后的语义Tableau定理证明器的推理效率得到了显着的提高.
叶育鑫[8]2010年在《语义Web下的知识搜索及其核心技术》文中研究表明搜索引擎无疑是当今计算机领域最炙手可热的关键词之一,它的出现和发展创造着业界无数的机遇和挑战。语义Web的兴起为搜索技术推波助澜,它一方面改变了旧的Web规范标准,实现了Web资源的机器可识别;另一方面它突破了以关键字为框架的传统Web搜索模式,将以字符匹配为特征的关键字搜索升级为知识搜索。本文研究语义Web下的知识搜索及其核心技术,以语义Web搜索框架下的Web资源获取、资源加工和生产、资源消费的智能信息处理流程为主线,分别讨论本体的增量一致性检测优化问题、基于语义的主题爬行问题、自动标注中的实体识别求精和语义生成问题、完整性约束本体的持久性存储问题、以及SPARQL语义查询中的优化问题,并考虑如何借助语义Web中的推理技术(本体推理)分析解决上述问题。这些问题的研究和解决有助于从各个环节和层面提升语义Web搜索能力,实现Web搜索智能化。本文研究内容主要包括:(1)分析本体推理在语义Web搜索框架中的作用和地位,提出一致性预处理优化和空间紧致优化策略,改进本体推理的核心任务之一——增量一致性检测的效率;(2)通过定义断言集一致性扩展和域值关联推理任务,推演关键词间语义关系,提出主题概念的语义迭加效应模型,利用主题概念的语义包含关系判定URLs抓取顺序,实现基于语义的主题爬行策略;(3)将本体推理中概念层次分级与机器学习中的k最近邻法相结合,研究语义Web自动标注中实体的识别求精和语义生成;(4)讨论完整性约束在本体到关系数据库映射中的作用和意义,研究基于完整性约束本体的持久性存储方法设计与实现;(5)研究语义Web资源的查询语言SPARQL查询优化问题,提出语义约简优化策略,并和选择估值策略相结合,进一步提升语义查询效率;(6)基于上述5项研究,研发面向语义Web的知识搜索系统——KS3W。
刘全, 孙吉贵[9]2006年在《基于Tableau的定理机器证明系统TableauTAP》文中研究说明使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP。该系统可以证明不含等词的经典逻辑公式和多值逻辑公式,通过预处理自动生成tableau规则,因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明,实验结果表明,TableauTAP在时间和空间效率上都是比较高的。
刘万伟[10]2009年在《扩展时序逻辑的推理及符号化模型检验技术》文中研究指明随着计算机软、硬件系统复杂性的日益增长,系统设计和实现的正确性越来越难以得到保证。因此,用以检验系统正确性的形式化方法亟待出现。上个世纪80年代提出的模型检验方法被证明是行之有效的系统正确性验证手段。执行模型检验的算法,对所采用规约语言的类型十分敏感。由于线性框架下的时序逻辑(如LTL),具有表达能力(相对)较强、直观、兼容性好等特点,使得这类时序逻辑在实际应用中被使用的相对广泛。但是,在工业界应用中,许多重要的时序性质无法采用LTL表达。因此,若干LTL的扩展被陆续提出,它们大致分为两类。1.一种方法是向时序逻辑中添加无穷多个时序连接子或者正规表达式,以期获得等价于ω-正规语言的表达能力。这类逻辑如ETL、FTL、PSL等。2.另一种方法是向时序逻辑中添加二阶量词或者不动点算子。这类时序逻辑诸如MSOL、QTL、线性μ-演算等。这些LTL的扩展,都与ω-正规语言等价。对于这些逻辑本身,人们比较关心下列问题:1.判定问题。即:逻辑的(可满足)判定性及其复杂度。这是在这些逻辑被提出时首先要解决的问题。2.公理化问题。即:能否给出一套针对该种逻辑的可靠完备的公理系统。公理系统往往由若干公理和推理规则构成。这些公理/规则刻画了该种逻辑的实质。3.模型检验问题。对于某种特定的时序逻辑,开发其高效的模型检验算法是人们追求的核心目标之一。同时,有无高效的检验算法也直接影响该种逻辑能否得到广泛应用。对于时序逻辑的各类ω-扩展,其公理化以及符号化模型检验算法的研究还具有另外的特殊意义。在线性结构上,等价于ω-正规语言的时序逻辑具有足够强的能力表达工业界实际应用中用到的各种性质。各种线性时间的时序逻辑,可以看作它们的逻辑片断或者子逻辑。因此,这些逻辑的公理化以及符号化模型检验算法可以派生出它的子逻辑或者实例的的公理系统和符号化模型检验算法。本文主要工作如下:1.给出了叁类ETL(ETLl、ETLf、ETLr)的可靠完备的公理系统,同时给出了基于时序算子编码的ETL逻辑片段可靠完备公理化方法。2.基于博弈方法,给出了μ-演算的公理系统的新的完备性证明。同已有的方法相比,该证明相对直观、简洁。3.基于tableau方法,给出了叁类采用交错自动机作为连接子的ETL(ATLf、ATLl、ATLr)以及PSL的某个变种(APSL)的基于BDD的符号化模型检验算法。4.分别给出了具有一般形式和特定形式(ν-范式)的线性μ-演算的基于BDD的符号化模型检验算法。5.基于上述算法,在模型检验工具NuSMV的基础上,实现了支持扩展时序逻辑的符号化模型检验工具ENuSMV。它允许用户通过描述自动机的方式自定义时序连接子,能够检验全部的ω-正规性质。
参考文献：
[1]. 基于tableau的自动推理技术综述[J]. 刘全, 孙吉贵, 于万钧. 计算机科学. 2005
[2]. 基于tableau的自动推理研究[D]. 刘全. 吉林大学. 2004
[3]. 基于tableau的数据记录匹配及一致性研究[D]. 李娇. 苏州大学. 2012
[4]. 一种基于集合符号的自动推理扩展方法[J]. 刘全, 伏玉琛, 孙吉贵, 崔志明, 龚声蓉. 计算机研究与发展. 2007
[5]. 若干逻辑自动推理方法研究[D]. 郭远华. 华东师范大学. 2009
[6]. Tableau基础理论及应用研究[D]. 王炜程. 苏州大学. 2009
[7]. 基于Tableau的定理证明器的优化技术研究[D]. 高华. 辽宁师范大学. 2015
[8]. 语义Web下的知识搜索及其核心技术[D]. 叶育鑫. 吉林大学. 2010
[9]. 基于Tableau的定理机器证明系统TableauTAP[J]. 刘全, 孙吉贵. 计算机工程. 2006
[10]. 扩展时序逻辑的推理及符号化模型检验技术[D]. 刘万伟. 国防科学技术大学. 2009
标签：自动化技术论文; 人工智能论文; 语义分析论文; 逻辑符号论文; web技术论文; 逻辑模型论文; tableau论文; 推理论文; 关系逻辑论文; 符号计算论文;