提高一阶多值逻辑Tableau推理效率的布尔剪枝方法

含有量词的一阶多值Tableau方法具有统一的扩展规则 ,并由Zabel等人给出了可靠性和完备性的证明 .但由于扩展后的分枝随着真值数目的增加而呈指数的增加 ,因而影响了机器推理执行的效率 .该文提出了布尔剪枝方法 ,将带符号的公式与集合的上集 /下集联系起来 ,使含量词的一阶多值逻辑公式的扩展规则大大简化 .进一步 ,通过对布尔剪枝方法的分析 ,建立了一类特殊一阶多值逻辑正则公式的更为简洁的Tableau推理方法 ,该方法使得含量词的一阶多值逻辑Tableau推理类同于经典逻辑Tableau方法 .

基于tableau的自动推理技术综述

tableau方法是一种接近于逻辑系统表示的自动推理方法,由于其直观性和通用性,易于计算机实现,成为目前最普及的自动推理方法之一。在提高系统效率方面,主要在相关技术和策略、理论和方法等方面进行了分析,并展望了未来的研究方向。

使用Tableau和Excel实现销售报告自动生成的原理与实践

文章介绍一种利用Tableau与Excel制作销售报告的高效方法。该方法结合Tableau与Excel这两种软件的优势,能自动生成报告中的统计分析图表及相应的文字表述内容,不仅速度快、效率高,而且灵活度高、准确度高,特别用于内容多变的销售报告。因方便、易用、操作简单,该方法可让非专业人员轻松使用。文章也以Tableau的样例数据为例,详细阐明如何用该方法自动生成一份销售报告。

基于Tableau的定理机器证明系统TableauTAP

使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP。该系统可以证明不含等词的经典逻辑公式和多值逻辑公式,通过预处理自动生成tableau规则,因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明,实验结果表明,TableauTAP在时间和空间效率上都是比较高的。

Tableau-based算法的改进与有限步终止定理

对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这个新算法,证明了ALCN语言中Abox的相容性可通过标准tableau-based算法在有限步之内判定.

动态描述逻辑的Tableau判定算法

动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.

从ALC到SHOQ(D):描述逻辑及其Tableau算法

描述逻辑是一类知识表示的形式系统,并成为语义Web的逻辑基础。Tableau是描述逻辑的基本证明论,基于Tableau的算法提供了描述逻辑的推理机。本文系统地阐述了对应于语义Web语言从基本的ALC到SHOQ(D)的描述逻辑基础及其相应的Tableau算法。

时态描述逻辑ALC-LTL的Tableau判定算法

时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-LTL中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。

自由变量语义tableau中δ-规则的一种改进方法

自动推理一直是人工智能领域研究的重要内容 近几年来 ,由于tableau方法的通用性和直观性 ,引起人工智能界的广泛关注 对于自由变量语义tableau中的量词规则 ,由于γ 规则替换的任意性 ,可导致在同一tableau证明中γ 规则被多次使用 ,使得tableau推理结构树中出现多个自由变量 针对tableau中多次出现自由变量 ,使tableau封闭延迟的问题 ,在δ+ 规则的基础上 ,提出对δ+ 规则改进的δ+ + 规则 ,并进行了正确性证明 将δ+ + 规则应用到TableauTAP系统中 ,结果表明 ,δ+ + 规则使tableau封闭提前 。

基于布尔剪枝的多值广义量词Tableau推理规则简化方法

Tableau作为自动推理的有效方法之一在许多领域中有重要的应用.该文作者在已提出的布尔剪枝方法基础上,对含广义量词(交和并)规则的简化方法进行研究,建立了一套含广义量词的一阶多值逻辑公式的简化Tableau推理方法.通过实例分析,对简化前后结果对比表明,改进后的Tableau方法,在推理效率上有很大的提高.

认识逻辑(3):基于语义tableau的证明理论

本文定义了带有索引的认识逻辑ELI，讨论了ELI的语义tableau的证明过程，证明了模态tableau的相容性和完备性．由于ELI与认识逻辑EL是等价的，因而，本文讨论的tableau证明过程也可以作为EL的证明理论．

Tableau算法的优化及模型规约技术

为了近一步提高模态逻辑推理机的效率,提出了两种Tableau算法优化技术——冲突技术和矛盾学习技术,并结合这两种技术实现了针对模态逻辑S4的推理机S4P.在此基础上,为了从Tableau算法生成的模型图中构造一个规模较小的模型,又提出通用模型的概念,然后给出通用模型的规约技术并证明该技术对于任意依赖于公理D、T、B、4和5中部分或全部公理的正规模态逻辑的正确性.最后,使用逻辑工作台测试用例对S4P的效率进行测试,实验结果表明S4P的效率优于RACER和FACT++;同时,对S4P生成的测试用例中非有效公式的否定对应的通用模型进行规约,实验结果表明通过模型规约能明显地缩减模型的规模.

非经典逻辑的语义tableau方法

1.引言 自动推理作为自动定理证明的扩展,在计算机科学,特别是人工智能领域中占有重要的地位.许多系统,都是以推理系统作为其核心部分,因此自动推理的研究,对人工智能的其它分枝将产生深远的影响,它所提出的推理方法也被应用于人工智能的各个领域.

一种逻辑强化学习的tableau推理方法

tableau方法是一种具有较强的通用性和适用性的推理方法,但由于函数符号、等词等的限制,使得自动推理具有不确定性.针对tableau推理中封闭集合构造过程具有盲目性的问题,提出将强化学习用于tableau自动推理的方法.该方法将tableau推理过程中的逻辑公式与强化学习相结合,产生抽象的状态和活动.这样一方面可以通过学习方法控制自动推理的推理顺序,形成合理的封闭分枝,减少推理的盲目性;另一方面复杂的推理可以利用简单的推理结果,提高推理的效率.

基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。

基于Tableau的标准起草单位大数据可视化分析

现有电子标准文献数据量大,每个标准文献都有其对应的起草单位等题录信息,针对标准和起草单位,在很多方面可以分析其中的关联关系,并通过不同的方式展现给读者,因此,本文利用Tableau软件对标准起草单位大数据进行多维度的可视化展示,使读者快速获取标准起草单位的各方面情况和更多标准信息资源背后隐含的价值,通过可视化分析结果能够更好地理解和使用标准,读者也能够更深刻地了解标准资源的起草和发展情况,提高了标准服务的效率。

一种基于语义tableau的数据库修正方法

tableau作为自动推理的有效方法之一在许多人工智能领域中有重要的应用。在tableau基础上,提出新的tableau开放和封闭的推理标准,应用于数据库实例不满足完整性约束的不相容关系数据库中,并对其进行修正。这样可以采用逻辑程序的方法,对数据库进行修正,解决了传统修正方法丢失信息、出现新的不相容等问题。

模糊命题模态逻辑的Tableau方法

为提高模糊命题模态逻辑(fuzzy propositional modal logic,FPML)的推理能力,本文将经典模态逻辑中的Tableau方法推广到FPML中,提出了基于FPML的Tableau规则并证明了其正确性,给出了模糊断言集合的约简策略;在此基础上给出了FPML中的不一致性和不一致估值的定义。最后给出基于Tableau方法的FPML的一致性检测方法 TFPML和模糊断言集合的不一致估值计算方法 CID,并证明了其正确性。实例分析表明,本文提出的方法是正确有效的。

ALC中的Tableau算法及其性质

描述逻辑是一族知识表示的形式化语言,是一阶谓词逻辑的可判定子集,已成为语义Web的理论基础。描述逻辑中ALC是最小命题封闭的,是其它描述语言的基础,而可判定是描述逻辑的最重要的问题,在ALC中Tableau算法巧妙地解决了这一问题,掌握ALC中的Tableau算法是理解各种描述逻辑中可判定性的基础。对ALC中的Tableau算法进行详细阐述,并对其关键的几个性质:可终止性、完备性和判定性给出了证明,为研究SHOIN(D)中的Tableau算法及性质奠定了基础。

基于模糊逻辑的不确定知识处理（Ⅱ）─—模糊逻辑的TABLEAU推理

本文基于ＴＡＢＬＥＡＵ方法，给出了模糊逻辑中一些至今缺少有效证明论的推理关系的证明论，也给出了作者提出的模糊择优蕴涵的判定过程．据此说明了Ｙａｇｅｒ所给出的推理规则对其所讨论的模糊推理关系是不完备的．分析了本文对前提和结论分别构造ＴＡＢＬＥＡＵ推理树的方法在研究推理关系的相关性等方面的直观语义和作为模糊Ｐｒｏｌｏｇ的推理机所具有的优越性．