一阶模糊谓词逻辑公式的有限解释真度和可数解释真度的理论及其应用

通过引进公式变元集赋值的新概念给出了一阶模糊谓词逻辑（或一阶模糊语言）公式的有限解释真度及可数解释真度的定义,并讨论了它们的一系列性质及其在近似推理中的应用,从而为一阶谓词逻辑的近似推理理论提供了一种带度量的框架.     

一阶谓词逻辑的图形推理法

针对已有一阶谓词逻辑推理方法中存在的推理效率低等问题,研究一种基于谓词/变迁系统的图形推理法。定义了描述谓词间与/或关系的谓词-与/或图,借助谓词-与/或图表示谓词/变迁系统,提出一种实现反向推理的目标制导的图形推理法。该方法推理效率高,较已有的推理方法具有一定的优越性。     

二值谓词逻辑中公式的向量真度

首次将谓词逻辑系统中一阶语言的有限解释按照其论域的势进行分层, 提出每一层解释类下公式的n真度, 最终给出公式向量真度的定义, 更直观精确地刻画一阶公式的真实程度。接着证明向量真度的一些基本性质, 指出向量真度保持谓词逻辑形式推理的MP规则、HS规则与推广规则, 从而为进一步在谓词逻辑系统中开展近似推理研究提供一种可能的框架。     

移动界程模型检测

首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中,提出了第1个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法,这也是目前已知的第2个带递归的谓词界程逻辑模型检测算法.所做的工作有:①讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性,给出了谓词界程逻辑公式转换成嵌套谓词等式系的方法;②讨论了谓词界程逻辑模型检测问题,给出了具体算法,并分析了算法的复杂性.     

计算机科学中的一些逻辑理论的推理性质研究

由于一阶 词逻辑的基本特征是具有可靠性,完全性,在推广一阶谓词逻辑表达能力及扩充其推理能力时,可以定义了了一些具有可靠性,完全性的逻辑,对此,在分析逻辑理论特征的基础上,给出了一些逻辑的推理系统之间相似性的实质,证明这些逻辑在实质上并不能扩充一阶谓词逻辑的推理能力,并指出非常单调推理中的缺省推理及限定推理所采用的技术是扩充时必需的。     

推广规则后一阶逻辑公式的准真度

计量逻辑理论是逻辑概念程度化研究方向的一个重要分支。但目前计量谓词逻辑的相关研究中，都不曾涉及推广规则。一阶逻辑公式的准真度理论是计量谓词逻辑的一个重要的研究成果，讨论经过推广规则后，一阶逻辑公式准真度的变化情况，证明经过推广规则后，一阶逻辑公式在基于准真度的一阶逻辑公式集的分类中类别不变。     

使用本体和SWRL验证作战计划的方法

计划验证是计划编制过程的重要环节。从知识管理的角度,在已有计划表示和计划推理相关研究的基础上,提出了一种基于本体和规则的计划验证方法框架,通过对计划知识进行基于本体的表示、基于描述逻辑、一阶谓词逻辑的规则知识抽取和计划推理,以实现对计划的验证。并以某排雷作战计划的验证为例进行了实验。实验表明,该方法实现了对专家知识的扩展,提高了作战计划正确性检验的效率。     

基于Markov逻辑网的虚假评论识别方法

为解决虚假评论识别的问题,该文提出一种基于Markov逻辑网的虚假评论识别方法。首先,对虚假评论内容和评论者行为的特点进行分析,选取评论内容特征和评论者行为特征;然后,根据特征定义一阶逻辑谓词和逻辑公式,并介绍了权重学习和推理的过程;最后,进行了对比实验,结果表明该方法的虚假评论识别取得了较好的效果。
     

基于逻辑映射的时空本体构造

时间和空间的表示和推理是人工智能研究中重要的组成部分。随着时空信息在地理信息系统、时空数据库、CAD/CAM等领域的重要应用,时空信息的本体表示越来越受到人们的重视。目前时空本体的构造都是基于一阶谓词逻辑,不能直接应用最新的OWL本体语言描述,不利于其在语义Web上的表示和应用。为解决这一问题,该文研究了使用一阶谓词逻辑到描述逻辑的逻辑映射构造的时空本体,给出了基于Web本体语言OWL的时空本体在Protégé环境中的具体实现。     

基于格值一阶逻辑LF（X）的自动推理算法

基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一。针对格值一阶逻辑LF(X)中归结自动推理问题,以格值一阶逻辑LF(X)的α-归结原理为理论基础,通过对例子进行分析,提出了LF(X)中简单广义子句集的归结自动推理算法,并证明了该算法的可靠性和完备性。     

利用谓词/变迁网证明的一阶谓词逻辑命题

研究了证明一般的一阶谓词逻辑命题的方法,根据网逻辑的思想,利用谓词/变迁网对一般形式的一阶谓词逻辑命题进行了图形表示,提出了2种一阶谓词逻辑命题的证明方法：图形证明法和矩阵证明法。举出一个实际的例子来说明证明思路。     

A recursive method for solving unconstrained tangentialinterpolation problems

An efficient recursive solution is presented for the one-sided unconstrained tangential interpolation problem. The method relies on the triangular factorization of a certain structured matrix that is implicitly defined by the interpolation data. The recursive procedure admits a physical interpretation in terms of discretized transmission lines. In this framework the generating system is constructed as a cascade of first-order sections. Singular steps occur only when the input data is contradictory, i.e., only when the interpolation problem does not have a solution. Various pivoting schemes can be used to improve numerical accuracy or to impose additional constraints on the interpolants. The algorithm also provides coprime factorizations for all rational interpolants and can be used to solve polynomial interpolation problems such as the general Hermite matrix interpolation problem. A recursive method is proposed to compute a column-reduced generating system that can be used to solve the minimal tangential interpolation problem     

Confirmation-Guided Discovery of First-Order Rules with Tertius

This paper deals with learning first-order logic rules from data lacking an explicit classification predicate. Consequently, the learned rules are not restricted to predicate definitions as in supervised inductive logic programming. First-order logic offers the ability to deal with structured, multi-relational knowledge. Possible applications include first-order knowledge discovery, induction of integrity constraints in databases, multiple predicate learning, and learning mixed theories of predicate definitions and integrity constraints. One of the contributions of our work is a heuristic measure of confirmation, trading off novelty and satisfaction of the rule. The approach has been implemented in the Tertius system. The system performs an optimal best-first search, finding the k most confirmed hypotheses, and includes a non-redundant refinement operator to avoid duplicates in the search. Tertius can be adapted to many different domains by tuning its parameters, and it can deal either with individual-based representations by upgrading propositional representations to first-order, or with general logical rules. We describe a number of experiments demonstrating the feasibility and flexibility of our approach.     

An intelligent modeling and analysis method of manufacturing process using the first-order predicate logic

Manufacturing process refers to machining sequence from raw materials to final products. Process plan has important effects on manufacturing process. In general, process designer relies on his experience and knowledge to arrange the process plan. For a complex part, it takes long time and effort to determine process plan. In this paper, an intelligent modeling and analysis method using the first-order predicate logic is proposed to evaluate the manufacturing performance. First, the logic predicates used to represent the process plan are defined according to the machining methods, and the predicate variables are discussed in detail. Consequently, the process plan can be represented in the form of the first-order predicate logic. Second, a type of element model composed of four nodes and four links is put forward in order to construct the process model. All components in this element model are respectively explained, and the mapping relationship between element model and predicate logic is described in detail. According to engineering practices, logic inference rules are suggested and the inference process is illustrated. Hence, the manufacturing process model can be constructed. Third, the process simulation is carried out to evaluate the performance of manufacturing system by using measures such as efficiency, the machine utilization, etc. Finally, a case study is given to explain this intelligent modeling method using the first-order predicate logic.     

Formalization of correctness of recursive definitions

We use the fixpoint approach to formalize the correctness of recursive definitions within the framework of first-order predicate calculus. Although the least fixpoint semantics is used, our results suggest some general methods of proving the correctness of recursive definitions without knowing their least fixpoints explicitly.