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

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

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

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

直觉模糊逻辑的（α,β）-广义锁归结方法

归结方法是定理自动证明的重要工具。为了简化直觉模糊命题逻辑的归结过程,基于直觉模糊命题逻辑归结原理的一般形式,提出了子句(αβ)-可满足和(αβ)-归结式的概念。研究了广义子句与其归结式的可满足性。在直觉模糊命题逻辑系统中给广义子句配锁,规定在做归结时各子句中被消去文字在该子句中的序号最小,由此建立了(αβ)-广义锁归结方法,并证明了该方法的可靠性和完备性。给出了直觉模糊逻辑的广义锁归结算法步骤,并通过实例说明了该方法的有效性。     

格值语义归结推理方法

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

直觉模糊逻辑的(α,β)-准锁语义归结方法*

为了提高直觉模糊命题逻辑的(α,β)-归结效率,将准锁语义归结策略应用于(α,β)-归结原理,得到直觉模糊命题逻辑的(α,β)-准锁语义归结方法,证明方法的可靠性与完备性.给出直觉模糊命题逻辑系统的(α,β)-准锁语义归结和(α,β)-准锁语义归结演绎的概念.讨论直觉模糊命题逻辑系统中的(α,β)-准锁语义归结式和锁子句的合并规则.最后,给出直觉模糊命题逻辑系统的基于(α,β)-准锁语义归结的自动推理算法步骤,并通过实例说明算法的有效性.     

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

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

广义模糊逻辑和锁语义归结原理

将命题的真值取在格上的模糊逻辑,我们称为广义模糊逻辑。本文讨论了这种广义模糊逻辑的性质,并证明了,对于一阶谓词公式,在广义模糊逻辑中的不可满足性和在二值逻辑中的不可满足性是等价的。还证明了原始的归结原理在广义模糊逻辑中是完备的。 最后,在模糊逻辑中讨论了涉及子句真值的语义归结原理,对于在广义模糊逻辑中的不可满足配锁子句集,在任意一个模糊解释下,使用语义归结原理,总可演绎出空子句。     

基于格值一阶逻辑LF（X）的多元α-归结原理的注记

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

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

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

基于算子模糊逻辑的不确定程度计算

本文提出并比较了在信度语义下，计算算子模糊逻辑中公式（集）模糊程度的3种方法——归结法、广义归结法和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.     

系统H_α中的子代数的广义重言式理论

将多值逻辑系统H(α0≤α≤1)中的广义重言式理论进行推广,讨论其序稠密子代数的广义重言式理论,利用可达广义重言式概念在系统H1的序稠密子代数中给出F(S)的一个分划,并把系统H1中的相关结论推广到系统H(α0≤α≤1)中。     

t-DeLP: an argumentation-based Temporal Defeasible Logic Programming framework

The aim of this paper is to propose an argumentation-based defeasible logic, called t-DeLP, that focuses on forward temporal reasoning for causal inference. We extend the language of the DeLP logical framework by associating temporal parameters to literals. A temporal logic program is a set of basic temporal facts and (strict or defeasible) durative rules. Facts and rules combine into durative arguments representing temporal processes. As usual, a dialectical procedure determines which arguments are undefeated, and hence which literals are warranted, or defeasibly follow from the program. t-DeLP, though, slightly differs from DeLP in order to accommodate temporal aspects, like the persistence of facts. The output of a t-DeLP program is a set of warranted literals, which is first shown to be non-contradictory and be closed under sub-arguments. This basic framework is then modified to deal with programs whose strict rules encode mutex constraints. The resulting framework is shown to satisfy stronger logical properties like indirect consistency and closure.     

基于零级泛与运算的泛逻辑中广义重言式理论

对泛逻辑的广义重言式理论进行了研究,给出了基于零级泛与运算的广义重言式的一系列性质。主要结果有:当c∈[0.75,1]时,关于Ih=c而言,F(S)中只有3种不同的广义重言式,即可达0-重言式、0+-重言式和重言式;当h=0时,关于Ih=0而言,F(S)中存在0、1可达重言式,当α∈(0,1),不存在α-重言式、α+-重言式和可达α-重言式;用h=0.5时的广义重言式对h∈(0,0.75)时的广义重言式进行了刻画。     

中介逻辑ML的语法完全性

中介逻辑ML(MediumLogic)是近年提出的一种非经典逻辑。在ML的系统特征理论中已证明ML具有语义完全(完备)性。本文研究了ML的语法完全性,证明了如下结果:(1)ML中的中介命题逻辑系统MP及其扩张MP*是语法完全的,中介谓词逻辑系统MF与其扩张MF*,以及含有等词的中介谓词逻辑系统ME不是语法完全的。(2)一般地,如果一个协调的逻辑形式系统不是语法完全的,则它的任何协调的扩张系统也不是语法完全的。     

An operational formal definition of PROLOG: a specification method and its application

We present in this paper a logic programming specification language and its application to the formal specification of PROLOG dialects (Marseille-Edinburgh like dialect or parallel logic programs). In particular it is used in the standardization work of PROLOG. The specification language is based on normal clauses (definite clauses with possibly negative literals in the body) whose semantics is the set of the (generalized) proof-trees. We restrict the specification language to stratified programs and ground proof-trees such that its semantics fits with most of the usual known semantics in logic programming. The specification language is fully declarative in the sense that it is written in a pure logical stule. It is relatively easy to deduce an executable specification from a specification written in such a language. Part of the specification are the associated comments and a methodology has been developed to write these. Without the comments a formal specification cannot be understood; they are partly formal and serve only to help to understand the axioms. They are a natural language form of formal statements relative to the correctness and the completeness of the axioms with regards to some intended meaning. We show in this paper how this specification language can be used to specify dialects of PROLOG. The presented example is just a sample of PROLOG but fully developed here. The specification language has already been used for real dialects as PARLOG and standard PROLOG. This specification method is also interesting because it illustrates the power of logic programming to make specifications. It seems to us that logic programming is generally considered as “impure” executable specification. Our purpose is to show that logic programming may also be used as a perhaps low level but full specification language.     

多值Łukasiewicz逻辑公式的范式表示和计数问题

将符号化计算树逻辑中的Shannon展开式做了推广,在n值Łukasiewicz逻辑系统Łn中,研究了由逻辑公式导出的n值McNaughton函数的展开式,给出了m元n值McNaughton函数的准析取范式和准合取范式.在此基础上,给出了m元n值McNaughton函数的计数问题,并在n值Łukasiewicz逻辑系统Łn中,给出了m元逻辑公式的构造方法及其逻辑等价类的计数问题.     

逻辑系统Hα中广义语义MP规则证明的改进

将修正的Kleene逻辑系统中语义MP规则推广后应用于H_α逻辑系统中,讨论了H_α逻辑系统中广义重言式理论的语义（[α]-MP）规则,语义（[α⁺]-MP）规则,使得对H_α系统中的广义语义MP规则有了更进一步的认识。另外,逻辑系统W中的广义语义MP规则也成为一个特例。     

Model checking for action-based logics

A model checker is described that supports proving logical properties of concurrent systems. The logical properties can be described in different action-based logics (variants of Hennessy-Milner logic). The tools is based on the EMC model checker for the logic CTL. It therefore employs a set of translation functions from the considered logics to CTL, as well as a model translation function from labeled transition systems (models of the action-based logics) to Kripke structures (models for CTL). The obtained tool performs model checking in linear time complexity, and its correctness is guaranteed by the proof that the set of translation functions, coupled with the model translation function, preserves satisfiability of logical formulae.