格值语义归结推理方法

归结自动推理是人工智能领域的一个重要研究方向,语义归结方法是对归结原理的一种改进,它利用限制参与归结子句类型和归结文字顺序的方法来提高推理效率。基于格蕴涵代数的格值逻辑系统的二归结原理提供了一种处理带有模糊性和不可比较性信息的工具,它能对格值逻辑系统中在一定真值水平下的不可满足逻辑公式给出反驳证明。首先研究了格值逻辑系统上一类广义子句集的性质,该类子句集在任意赋值下能分为两个非空子集,接着讨论了这类广义子句集的语义归结方法,并证明了其可靠性和完备性。     

语言真值格值命题逻辑中的α-语义归结方法

语言值智能信息处理是人工智能的一个重要研究方向,基于归结原理的自动推理因易于在计算机上实现而得到广泛研究。为了提高基于语言真值格值逻辑的α-归结原理的效率,将语义归结策略应用于α-归结原理,研究了基于格值逻辑的归结自动推理方法。首先给出了语言真值格值命题逻辑系统的α-语义归结与L_nP(X)中相应归结水平的语义归结之间的等价性,并通过实例说明其有效性。接着,给出了语言真值格值命题逻辑系统的α-语义归结算法,并证明了该算法的可靠性和完备性。     

格值一阶逻辑LF(X)中的α-语义归结方法

自动推理是人工智能的一个重要研究方向,基于归结原理的自动推理因易于在计算机上实现而得到广泛研究。语义归结是对归结原理的一种改进,它利用限制参与归结子句类型和归结文字顺序的方法来提高推理效率。为了提高基于格蕴涵代数的格值逻辑的α-归结原理的效率,将语义归结策略应用于α-归结原理。首先给出了格值一阶逻辑系统中的α-语义归结概念和α-语义归结演绎概念,接着讨论了格值一阶逻辑系统的α-语义归结方法,并证明了其可靠性和条件完备性,最后通过实例说明了其有效性。     

基于格值命题逻辑系统LP(X)的多元α-归结原理的注记

进一步深入研究了基于格蕴涵代数的格值命题逻辑系统LP(X)的多元α-归结原理的基本理论,给出了基于LP(X)的多元α-归结演绎中参与多元α-归结的广义文字个数随着归结演绎的推进而动态变化的基本原则;对基于LP(X)的多元α-归结原理的有效性进行了一定分析,这为建立基于LP(X)的多元α-归结方法以及构造多元α-归结算法奠定了理论基础.     

格值命题逻辑系统L9P(X)中的自动推理算法

给出了格值命题逻辑系统L₉P（X）上的放缩原理和放缩归结原理,基于放缩归结原理,给出了一种判断L₉P（X）上子句集S为M－可满足的自动推理算法（这里M为L₉上的中界元）,并证明了其可靠性和完备性。     

语言真值格值命题逻辑系统中广义文字的归结判定

自动推理是人工智能研究的一个重要内容,基于归结原理的自动推理是自动推理研究的重要分支。基于语 言真值格蕴涵代数的格值逻辑系统能处理带有可比较项和不可比较项的信息或知识,为自动推理研究提供了严格的 逻辑基础。给出了语言真值格蕴涵代数纷相似文献   

命题逻辑中非子句α-有序线性广义归结方法

为了处理在不确定性环境下的自动演绎,重点研究了基于自动推理理论的归结方法,其自动推理理论是真值定义在格蕴涵代数（lattice implication algebra,LIA）结构上格值逻辑系统中的。在已有的确定真值水平α二元归结研究的基础上,作为其继续研究和扩展,引入了基于格值命题逻辑系统LP( X )的非子句多元α-有序线性广义归结方法和演绎,这从本质上避免了一个非子句广义归结演绎到规范子句的形式。随后,得到LP( X )中的非子句多元α-有序线性广义归结演绎是可靠和完备的。该研究工作为格值命题逻辑中基于自动推理的归结提供了一个更有效的方法。     

基于语言真值格值命题逻辑系统(e)vpl的推理规则

一个逻辑系统在实际应用中,推理规则的选取往往很重要.本文基于语言真值格值命题逻辑系统ípl,提出了几种推理规则,这些推理规则包含有语义和语法,且它们之间具备协调水平的特性,证明了推理规则在一定程度上具备闭性特性.     

基于语言真值格值命题逻辑系统lvpl的推理规则

一个逻辑系统在实际应用中,推理规则的选取往往很重要。本文基于语言真值格值命题逻辑系统lvpl,提出了几种推理规则,这些推理规则包含有语义和语法,且它们之间具备协调水平的特性,证明了推理规则在一定程度上具备闭性特性。     

分层格值命题逻辑系统中几类推理规则的讨论

在基于格值逻辑的不确定性推理的研究中,推理规则的选取是其重要研究内容之一。基于分层格值命题逻辑系统,提出了几类既包含有语义又含有语法的推理规则,且这些推理规则具备协调水平的特性;同时也证明了这几类推理规则在一定程度上有闭性。     

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

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

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.     

Determination of α-resolution in lattice-valued first-order logic LF(X)

Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure-lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called α-resolution) in LF(X) is proved to be equivalently transformed into the determination of α-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of α-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of α-resolution in LF(X) can be accordingly solved to a very broad extent, which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X), but also provides a key support for α-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.     

-Resolution principle based on lattice-valued propositional logic LP(X)

In the present paper, resolution-based automated reasoning theory in an L-type fuzzy logic is focused. Concretely, the -resolution principle, which is based on lattice-valued propositional logic LP(X) with truth-value in a logical algebra – lattice implication algebra, is investigated. Finally, an -resolution principle that can be used to judge if a lattice-valued logical formula in LP(X) is always false at a truth-valued level (i.e., -false), is established, and the theorems of both soundness and completeness of this -resolution principle are also proved. This will become the theoretical foundation for automated reasoning based on lattice-valued logical LP(X).