BL*系统和IMTL系统等价性的语构证明

BL*命题演算形式演绎系统和IMTL命题演算形式演绎系统是从不同的角度出发建立的两种基础模糊命题演算的形式演绎系统。对两者进行了较细致的比较研究,从语构方面证明了两种命题演算形式演绎系统的等价性,从而进一步明确了基础命题演算形式演绎系统BL*系统,MTL系统,BL系统,IMTL系统之间的联系,为各种模糊命题演算形式演绎系统的研究提供了一个有益的参考。     

逻辑系统L_n*中一类特殊公式的Σ_Γ-真度

在模糊命题系统L_n~*中,利用公式A的原子公式集S_A与有限理论Γ的原子公式集S_Γ之间的关系,讨论了公式A的Σ_Γ-真度,给出了当S_ΓS_A和S_A∩S_Γ=Φ时τ_Γ(A)的简单表示形式。利用这些结论,给出了当S_ΓS_A时Σ_Γ-真度的一些性质的简单证明。     

广义非线性系统解的一致最终有界性研究*

首先利用隐函数定理及常规的非线性系统解地存在唯一性定理,给出了广义非线性系统解的存在唯一性条件,然后利用标量和Ｌｙａｐｕｎｏｖ函数方法,从系统本身出发,研究了广义非线性系统解的一致最终有界性。     

相干命题逻辑自然推理系统NR的自动证明*

给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列。对系统NR的大部分定理证明取得了良好的效果,算法生成的演绎序列清晰可读,接近手工推理。     

TwigStar——快速处理XML Twig查询中含通配符*的算法

XMLTwig查询可以表示为一棵带标签结点的查询树,它支持对XML文档进行带有复杂谓词的结构或内容查询.整体(holistic)Twig查询算法已经被公认为XML查询处理的核心算法.很多学者提出了大量基于整体处理的XML Twig查询算法.但是目前已有的算法都只适合于Twig查询中不包含通配符*的情况.而当Twig查询中包含通配符*时,一种简单而直接处理的方法就是,把被查询文档中的所有结点元素都读到内存,把这些元素都看做通配符*所对应的元素,然后按照已有的算法进行查询处理.显然这种方法是不合理的,它会增加大量I/O开销.因此提出了一种有效地支持通配符*的查询处理算法.通过建立索引,它可以很好地处理含通配符*的查询,从而可以避免不必要的I/O开销.最后通过实验证明,算法要明显好于已有的算法.     

一种针对邮件服务类应用改进的2Q*算法及其在存储缓存中的应用

针对2Q算法对于邮件服务类负载所表现出的缓存性能特点提出了一种改进算法2Q*。模拟实验数据显示,改进后的2Q*算法在各种缓存容量下都优于包括经典2Q算法在内的其他替换算法。为了验证2Q*算法在真实系统中的有效性,将该算法集成于FlexiCache系统中并与目前主流的顺序自适应预取策略有机结合。实验结果表明,2Q*算法不仅能够在实际缓存系统中有效改善邮件服务类应用的物理I/O性能,而且其实际运行开销也非常低。     

基于A*引导域的RRT智能车辆路径规划算法

为了泛化RRT （快速搜索随机树）算法在智能车辆路径规划领域内的应用,解决该算法搜索效率低、最近邻搜索函数不合理等问题,本文提出了一种基于A*引导域的RRT路径规划算法.该算法将A*算法与RRT搜索算法进行有效地结合,利用由A*算法在低分辨率栅格图中生成的最短路径来构建引导域,以提升RRT算法的采样效率;同时在设计RRT算法的最近邻搜索函数时考虑车辆自身约束,以增强搜索树节点选择的合理性.通过仿真实验和实车测试,对该算法的优越性、有效性和实用性进行了验证.     

基于规范演绎的结构式程序综合

本文中提出一个用于程序综合的构造证明系统,规范演绎.这是一个层次化的由规范推导到定理证明的演绎系统.基于这种方法,程序综合成为一个结构式的证明过程.用逻辑程序的自动综合为例展示了这些方法.     

基于节点优化与清洗的改进A*路径规划算法

针对传统A*算法利用OpenList和CloseList进行路径规划时存在冗余节点数量多、部分转角节点可被删除的情况,提出一种基于节点优化与清洗的改进A*路径规划算法.改进A*算法首先对已规划路径进行优化,包括删除直线段路径的中间节点,并判断障碍物到规划路径的距离,删除最小距离大于0的可省略转角节点,从而保证用于路径规...     

逻辑系统L*中公式的Γ-演绎真度理论

在命题逻辑系统L*中引入了公式的Γ-演绎真度概念,研究了Γ-演绎真度的若干特征性质,并给出了真度推理规则。     

基于目标演绎距离的一阶逻辑子句集预处理方法

一阶逻辑定理证明是人工智能的核心基础,研究一阶逻辑自动定理证明器的相关理论和高效的算法实现具有重要的学术意义。当前一阶逻辑自动定理证明器首先通过子句集预处理约简子句集规模,然后通过演绎方法对定理进行判定。现有的应用于证明器中的子句集预处理方法普遍只从与目标子句项符号相关性角度出发,不能很好地从文字的互补对关系中体现子句间的演绎。为了在子句集预处理时从演绎的角度刻画子句间的关系,定义了目标演绎距离的概念并给出了计算方法,提出了一种基于目标演绎距离的一阶逻辑子句集预处理方法。首先对原始子句集进行包含冗余子句约简并应用纯文字删除规则,然后根据目标子句计算剩余子句集中的文字目标演绎距离、子句目标演绎距离,并最终通过设定子句演绎距离阈值来实现对子句集的进一步预处理。将该预处理方法应用于顶尖证明器Vampire,以2017年国际一阶逻辑自动定理证明器标准一阶逻辑问题组竞赛例为测试对象,在标准的300 s内,加入提出的子句集预处理方法的Vampire4.1相比原始的Vampire4.1多证明4个定理,能证明10个Vampire4.1未证明的定理,占其未证明定理总数的13.5%;在证明的定理中,提出的子句集预处理方法能对77.2%的子句集进行约简,最大子句集约简规模达到51.7%。实验结果表明,提出的一阶逻辑子句集预处理方法是一种有效的方法,能有效地约简一阶逻辑子句集的规模,提高一阶逻辑自动定理证明器的证明能力。     

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

Natural Deduction for First-Order Hybrid Logic

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.     

Mathematical Programming Embeddings of Logic

Can theorem proving in mathematical logic be addressed by classical mathematical techniques like the calculus of variations? The answer is surprisingly in the affirmative, and this approach has yielded rich dividends from the dual perspective of better understanding of the mathematical structure of deduction and in improving the efficiency of algorithms for deductive reasoning. Most of these results have been for the case of propositional and probabilistic logics. In the case of predicate logic, there have been successes in adapting mathematical programming schemes to realize new algorithms for theorem proving using partial instantiation techniques. A structural understanding of mathematical programming embeddings of predicate logic would require tools from topology because of the need to deal with infinite-dimensional embeddings. This paper describes the first steps in this direction. General compactness theorems are proved for the embeddings, and some specialized results are obtained in the case of Horn logic.     

Theory of truth degrees of propositions in the logic system L_n~*

Approximate reasoning based on the idea of fuzzy sets was firstly proposed by Zadeh[1] in 1973, which differs from the one advocated in Artificial Intelligence. Indeed, Artificial Intelligence emphasizes symbolic manipulation and roots itself in logic, em…     

Modal logic as metalogic

The goal of this paper is to show how modal logic may be conceived as recording the derived rules of a logical system in the system itself. This conception of modal logic was propounded by Dana Scott in the early seventies. Here, similar ideas are pursued in a context less classical than Scott's.First a family of propositional logical systems is considered, which is obtained by gradually adding structural rules to a variant of the nonassociative Lambek calculus. In this family one finds systems that correspond to the associative Lambek calculus, linear logic, relevant logics, BCK logic and intuitionistic logic. Above these basic systems, sequent systems parallel to the basic systems are constructed, which formalize various notions of derived rules for the basic systems. The deduction theorem is provable for the basic systems if, and only if, they are at least as strong as systems corresponding to linear logic, or BCK logic, depending on the language, and their deductive metalogic is not stronger than they are.However, though we do not always have the deduction theorem, we may always obtain a modal analogue of the deduction theorem for conservative modal extensions of the basic systems. Modal postulates which are necessary and sufficient for that are postulates of S4 plus modal postulates which mimic structural rules. For example, the modal postulates which Girard has recently considered in linear logic are necessary and sufficient for the modal analogue of the deduction theorem.All this may lead towards results about functional completeness in categories. When functional completeness, which is analogous to the deduction theorem, fails, we may perhaps envisage a modal analogue of functional completeness in a modal category, of which our original category is a full subcategory.     

A note on Trillas' CHC models

Trillas et al. [E. Trillas, S. Cubillo, E. Castiñeira, On conjectures in orthocomplemented lattices, Artificial Intelligence 117 (2000) 255-275] recently proposed a mathematical model for conjectures, hypotheses and consequences (abbr. CHCs), and with this model we can execute certain mathematical reasoning and reformulate some important theorems in classical logic. We demonstrate that the orthomodular condition is not necessary for holding Watanabe's structure theorem of hypotheses, and indeed, in some orthocomplemented but not orthomodular lattices, this theorem is still valid. We use the CHC operators to describe the theorem of deduction, the theorem of contradiction and the Lindenbaum theorem of classical logic, and clarify their existence in the CHC models; a number of examples is presented. And we re-define the CHC operators in residuated lattices, and particularly reveal the essential differences between the CHC operators in orthocomplemented lattices and residuated lattices.     

容纳矛盾逻辑系统与悖论

分析了目前各种容纳矛盾逻辑系统的不足,提出了正域、反域、不动域的概念,进而发现悖论是逻辑思维领域的不动点,建立了一个容纳矛盾的逻辑系统S,并给出了系统S的语义模型,证明了系统S的元定理.在系统S中,命题演算被分成3个独立的域,正域、反域中所有经典逻辑的定理与演算模式都是有效的;不动域是一个包含矛盾的域,在不动域中,可以证明悖论是一个定理.系统S与Da Costa的次协调逻辑系统Cn相比较,它不但可以容纳矛盾,并且可以把矛盾解释清晰.以此逻辑系统为基础,可以建立一个容纳矛盾的数学基础.     

A modal logic internalizing normal proofs

In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems.     

泛逻辑的基本形式演绎系统UL及其可靠性

1 引言自Zadeh于1965年建立模糊集理论以后,一种初始形态的模糊逻辑也被提出。尽管模糊推理在模糊控制中有直接的应用,也受到模糊系统与人工智能学界的广泛关注,但是,由于模糊推理长期以来没有严格的逻辑基础,致使其进一步发展受到限制,且不可避免地受到怀疑与批判。不过,近年来,以王国俊教授为首的一批学者成功地将模糊逻辑和模糊推理结合起来,通过建立模糊逻辑的形式演绎系统、创建模糊推理的三I算法等一系列漂亮的工作,极大地推动了这一领域向理论和应用的纵深发展。