一种基于集合符号的自动推理扩展方法

在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.     

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

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

一种基于语义Tableau的不相容知识处理方法

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

一般术语公理下的模糊描述逻辑FALCN推理

分析了一般术语公理下推理的主要难点:在模糊解释中的隶属度不是离散值,而是区间[0,1]上的连续值.为解决该难点,提出了模糊描述逻辑FALCN下的模糊解释离散化方法,从而使解释中的隶属度都属于一个特殊的有限离散集合.基于该离散化方法,给出一般术语公理下FALCN推理问题的离散Tableau推理技术,包括离散Tableau的定义以及离散Tableau的构造算法,并证明了算法的正确性、完备性和复杂度.     

粗描述逻辑RALCQ的Tableau推理

基于描述逻辑ALCQ,通过引入分级近似算子而得到粗描述逻辑RALCQ。随后通过转换的方法得到粗描述逻辑RALCQ的Tableau算法推理规则及推理复杂性。     

模糊专家系统中量词的推理方法

分析模糊专家系统包含的隐性知识,即量词在模糊推理过程中的推理难度。根据量词在命题中的位置,将其分为2种情况进行讨论。提出通过查表实现量词推理的方法,阐述2种情况下查询表的建立原理。该方法可以避免模糊推理计算的复杂性。     

动态描述逻辑推理的并行计算技术

在设计用于处理大规模本体和数据的推理引擎时,推理引擎的可扩展性是一个需要研究的重要问题.动态描述逻辑要在真实环境中获得成功应用,需要在推理中采用并行计算技术.提出了两种方法将并行计算技术应用于动态描述逻辑推理.方法1是设计分布式动态描述逻辑框架.分布式动态描述逻辑由若干独立的动态描述逻辑所组成,这些动态描述逻辑两两之间通过桥规则联系起来.提出了基于Tableau的分布式推理算法,从而为分布式动态描述逻辑提供了全局推理能力,并且该算法可以将大的推理任务分解为若干子任务,而这些子任务可以被不同的推理主体并行处理.方法2是并行化动态描述逻辑的Tableau算法的不确定分支.不确定分支的并行计算使得推理任务可以在若干独立机器上同时执行.最后,介绍了推理引擎的原型实现并评估了其性能.实验结果表明提出的两种方法取得了明显的推理加速效果.     

形式化模糊量词及推理

带有模糊量词的推理在计算机科学特别是人工智能中十分重要。模糊量词具有“统计”的性质,本文将从此角度讨论模糊量词的形式化及带有模糊量词的推理,本文的结果可应用在专家系统等智能系统中。     

一种带缺省推理的描述逻辑

该文提出了一种新的带缺省推理的描述逻辑，它以描述逻辑为主要框架，对单调逻辑和非单调逻辑进行了整合，但又避免了一般缺省逻辑的困难．基于带缺省推理的描述逻辑，构建了一种同时具有Tbox，Abox和缺省规则的知识库系统，研究了带缺省推理的描述逻辑的可满足性、缺省可满足性、概念包含、缺省包含以及实例检测等推理问题，提出了一种用来检测可满足性和缺省可满足性的Tableau—D算法，并得到了缺省可满足性和缺省包含的转换定理．     

模块化本体的Tableau算法及其性能优化

针对现有模块化本体推理方法通用性低、控制复杂等不足,提出一种基于服务的分布式Tableau算法。模块在进行一致性推理时,对关于外部概念的断言,将调用相应模块的服务进行推理,同一推理中的矛盾在定义相应概念的模块中得到捕获,采用优化技术改进算法的时间性能。实验结果表明,该算法使得模块在表述知识时能灵活引用外部概念,支持复杂的推理任务,具有较好的可伸缩性。     

一种多值规则量词公式的tableau的方法

在多值逻辑中，含有量词的tableau方法具有统一的扩展规则，并已通过可靠性和完备性的证明。但是由于扩展后的分枝非常庞大，使机器实现非常困难。文章通过对规则量词公式与一阶经典量词公式的对应关系的研究，使二者使用统一的扩展规则。     

Analogic: Inference beyond logic

Analogic is the unique class of many-valued, non-monotonic logics which preserves the richness of inferences in (Boolean) logic and the manipulability of (Boolean) algebra underlying logic, and, in addition, contains a number of unexpected, emergent properties which extend inferentiability in non-trivial ways beyond the limits of logic. For example, one such inference is rada (reductio ad absurdum, reasoning by contradiction, but now in the absence of excluded middle). This is important to retain since direct proofs of many theorems are not known. Another example is chaining. Transitivity is uncommon in many-valued logics; however, in analogic we can carry out inferences in either direction even through weak links in the chain. The latter, impossible in logic, simulate intuitive leaps in reasoning. Protologic effects inferences using only (n+1) implications which require 2ⁿ implications in logic. Indeed protologic has no counterpart in logic, or any other form of reasoning. Analogic is useful in formulating problems which are largely inferential including document and pattern classification and retrieval. These inference properties, long sought after in alternative logics by adding appropriate axioms or other indicative implicit or explicit restrictions, are now available in analogic, in turn the result of removing an axiom and letting inferences become many-valued.     

Efficiently solving quantified bit-vector formulas

In recent years, bit-precise reasoning has gained importance in hardware and software verification. Of renewed interest is the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifier-free fragment of bit-vector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bit-vector formulas to avoid an exponential blow-up during construction. Solvers for quantified formulas usually flatten the input to obtain a quantified Boolean formula, losing much of the word-level information in the formula. We present a new approach based on a set of effective word-level simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on skeletons/templates. Experimental results on two different types of benchmarks indicate that our method outperforms the traditional flattening approach by multiple orders of magnitude of runtime.     

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

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

Graded consequence: an institution theoretic study

We develop a general study of graded consequence (of many-valued logic) in an institution theoretic (in the sense of Goguen and Burstall) style. This means both syntax and semantics are considered fully abstract, as well as the satisfaction between them. Our approach contrasts to other approaches on many-valued logic in that it is a multi-signature one, in the spirit of institution theory. We consider graded consequence at three different conceptual levels: entailment, semantic, and closure operators, and explore several interpretations between them. We also study logical connectors and quantifiers both at the entailment and semantic level, compactness and soundness properties.     

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

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

Filter-based resolution principle for lattice-valued propositional logic LP(X)

As one of most powerful approaches in automated reasoning, resolution principle has been introduced to non-classical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logic is a kind of important non-classical logic, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP(X) based on lattice implication algebra is presented, where filter of the truth-value field being a lattice implication algebra is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP(X) are given firstly. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given and after that the soundness theorem and weak completeness theorems for the presented approach are proved.     

The Expressive Power of Finitely Many Generalized Quantifiers

We consider extensions of first order logic (FO) and fixed point logic (FP) by means of generalized quantifiers in the sense of Lindström. We show that adding a finite set of such quantifiers to FP fails to capture PTIME, even over a fixed signature, strengthening earlier results. We also prove a stronger version of this result for PSPACE, which enables us to establish that PSPACE ≠ FO on any infinite class of ordered structures, a weak version of the ordered conjecture formulated by Ph. G. Kolaitis and M. Y. Vardi (Fixpoint logic vs. infinitary logic in finite-model theory, in "Proceedings, 7th IEEE Symposium on Logic in Computer Science, 1992," pp. 46-57). These results are obtained by defining a notion of element type for bounded variable logics with finitely many generalized quantifiers. Using these, we characterize the classes of finite structures over which the infinitary logic L^ω_∞ω extended by a finite aw set of generalized quantifiers Q is no more expressive than first order logic extended by the quantifiers in Q.