模态逻辑的计量化研究及其在模型检验中的应用
|
摘要
本文的目的在于建立模态逻辑的计量化理论,并将其基本方法用于解决模型检验的计量化问题以及简化模型检验的过程.
计量逻辑学的提出旨在将基于概率、积分等工具的数值计算方法引入到以形式推理为特色的数理逻辑中,使原本符号化的推理具备某种灵活性从而扩展其应用范围.这种思想的雏形最初见于从逻辑语义基本概念的程度化入手而在若干命题逻辑系统中所建立的公式真度理论.此后引发了大量的后续研究,包括对逻辑度量空间的拓扑性质与内蕴结构的研究、对逻辑理论的发散度与相容度的研究以及在命题逻辑中建立近似推理的研究等,至今已形成了较为完善和成熟的计量逻辑学理论.如今计量逻辑学的研究对象已从命题逻辑的范围扩展到了表达力更强的模态逻辑、时态逻辑与谓词逻辑的理论之中.若干将计量逻辑学与其他领域相结合的创新性研究也不断涌现,显示出了计量逻辑学的旺盛生命力与广阔的应用前景.本文的研究目的在于探索计量逻辑学与理论计算机科学的新的结合点,将原本在命题逻辑中行之有效的计量化方法向表达力更强的模态逻辑与时态逻辑中推广,并尝试将其应用于以时态逻辑为逻辑背景的模型检验理论之中.
模态逻辑是非经典数理逻辑与人工智能理论相结合的一个重要方面.它不仅是时态逻辑、知识推理的理论基础,又常在应用中作为程序语义描述的工具.作为命题逻辑的模式扩张,模态逻辑具有命题逻辑所不具备的特点.例如模态逻辑中有若干可以表达“可能”、“必然”以及“将来”、“过去”等不同类型概念的模态词,随着模态词的增多,模态逻辑的表达能力也随之增强,此外局部概念的引入以及可能世界之间关系的论述等也使得模态逻辑具有比命题逻辑强得多的表达能力.正是由于这些特点,使得将原本在命题逻辑中行之有效的计量化方法向更为广泛的模态逻辑中推广成为了近几年计量逻辑学的基本研究任务之一.本文将从模态逻辑Kripke语义的局部化特点出发,建立模态公式的局部化真度,继而再利用某种聚合的方法将其推广为模态公式的全局真度,从而在模态逻辑中建立起较为广泛的计量逻辑理论.
另一方面,模型检验是一种形式化的认证方法,可以用来自动地检验某系统的模型是否满足为该系统设定的规范.这一理论已经经历了迅速发展的三十年,受到了人工智能学界的广泛关注,如今已被成功地应用于包括工业、金融、医疗乃至航空航天等重要领域.注意到模型检验理论的逻辑背景是某类特殊的时态逻辑,它们可以看作是模态逻辑的模式扩张.基于这些考虑,本文将进一步把针对模态逻辑的计量化理论向这类时态逻辑中推广,从一个全新的角度建立模型检验中的计量化理论,并讨论如何针对特殊类型的公式来简化模型检验的过程.
全文共分为五章：
第一章首先简要介绍有关命题逻辑的若干预备知识,包括语构理论、语义理论和完备性问题,并介绍几种常用的命题逻辑系统；然后从分析将基本逻辑概念进行程度化的必要性入手,简要介绍计量逻辑学的基本理论,包括公式的真度、公式之间的相似度、公式集上的伪距离以及逻辑度量空间等理论.
第二章首先简要回顾基本模态逻辑的语义理论、语构理论以及完备性问题；其次对基本模态逻辑的Kripke语义进行推广,将基本模型中的赋值域扩充为完备格,从而建立格值模态逻辑的Kripke语义,并证明该语义也将模糊模态逻辑的Kripke语义纳入其框架之下；然后以Boole代数为背景建立Boole型格值模态逻辑系统B,讨论系统B的语义理论与语构理论,并证明完备性定理的成立,即,任一模态公式是系统召中的定理当且仅当它是有效公式,同时指出基本模态逻辑的Kripke模型实际上是本文所提出的Boole型模态模型的特例；最后提出QMR0代数的概念,并以QMR0代数为背景构建QMR0型格值模态逻辑系统QML*讨论系统QML*的语义理论与语构理论,并证明完备性定理的成立,同时指出模糊模态逻辑的Kripke模型实际上是本文提出的QMRo型模态模型的特例.
第三章首先以单位区间[0,1]的有限子集作为赋值域,建立多值模态逻辑的Kripke模型以及相应的语义理论,并指出这种模型一方面是第二章提出的格值模态模型的特例,同时其Kripke语义又将基本模态逻辑的Kripke语义纳入其框架之下;其次采用固定可能世界集W与二元关系R而让赋值映射自由变动的方法建立。型框架,并在该框架下用归纳的思想构建模态公式关于某个可能世界诱导的局部化映射,从而引入模态公式的局部化真度概念,证明了这种局部化真度满足约简定理,即,任一模态公式的局部化真度均可以转化为另一个不含模态词的公式在同一可能世界处的局部化真度,从而达到简化真度计算的目的;然后进一步利用聚合的方法将这种局部化真度推广为模态公式的全局真度,并证明全局真度满足一致性定理,即,当某模态公式不含模态词时,其全局真度与其在命题逻辑中的真度一致：同时证明了模态公式的局部化真度值与可能世界集的势并无关系,且其全局真度能够较好地反应时态逻辑的语义特点；最后引入模态公式之间的相似度与伪距离.从而建立起多值模态逻辑度量空间,并证明基于命题逻辑的度量空间是多值模态逻辑度量空间的子空间.
第四章首先简要回顾模型检验理论中有关迁移系统以及线性时态逻辑LTL的基本概念；其次在有限迁移系统的全体无穷初始路径之集上引入某种适当的均匀概率测度.并基于该测度考虑迁移系统TS中满足某个LTL公式φ的路径占总路径的比例,从而定义迁移系统TS对于公式φ的满足度,即TS满足φ的程度,同时在此基础上引入LTL公式之间的相似度与伪距离,并构建线性时态逻辑中的度量空间,即LTL逻辑度量空间；然后将以上建立的满足度理论进一步推广至迁移系统的随机化模型,即离散时间马尔可夫链模型,并类似地引入LTL公式的满足度、相似度与伪距离等概念.此时不再要求各个状态之间相互迁移的概率是等值分布的.从而全体无穷初始路径之集上的概率测度也不是均匀分布的；最后引入线性时态逻辑中公式的特征与时态范式等概念,指出存在特征的LTL公式在模型检验中总可以在有限步内判断其有效性,即使相应的迁移系统含有无限多个状态时也是如此,并证明了LTL公式有与其等价的时态范式当且仅当其存在特征,从而一类特殊的LTL公式可以用线性时态逻辑的有界情形LTLn来刻画.
第五章首先在一般Boole代数中引入推演元的概念,并针对Boole代数建立相应的协调集理论;其次在一般Boole代数中引入反驳、极大缩减、极小减集等概念,并分别给出Boole代数中求某个有限不协调集的全体极小不协调子集以及求有限个集合的全体极小选择的算法原理,从而给出求全体极大缩减的方法,同时指出在一阶语言范围内求全体R-缩减的问题可以转化至Boole代数的范围内求解;最后在Boole代数中引入基本元的概念,并将子句及Horn子句等概念移植到一类由基本元生成的特殊Boole代数中,从而在这类特殊Boole代数中给出求子句集的全体极大缩减的算法原理,同时指出经典二值命题逻辑中求子句集(特别是Horn子句集)的全体R-缩减的问题可以转化至由基本元生成的Boole代数范围内求解.
This thesis aims at exploring quantitative approaches for modal logic as well as model checking. As an application, it also attempts to find a way to simplify the complexity of model checking systems.
Quantitative Logic focuses on the combination of formal inference and numerical calculation methods, such as probability and integral, in mathematical logic theory to make it more flexible and applicable. Such research was initially formed by grading basic logical concepts in several propositional logics in order to construct truth degree theory for formulae. Later on, a large number of subsequent research grew up, in-cluding topological and intrinsic structure analysis for logic metric spaces, divergence and consistence degree study for logical theories as well as construction of approxi-mate reasoning in propositional logic. Nowadays, Quantitative Logic not only owns systematic and mature theory within the scope of propositional logl its research sub-jects also cover more expressive logics, such as modal logic, temporal logic and even predicate logic. Besides, various kinds of investigation appear with innovation, which are devoted to combining Quantitative Logic and other related research fields. This thesis aims at exploring a new joint for Quantitative Logic and theoretical computer science. To be more specific, the quantitative approach used in propositional logic will be extended in the range of modal logic as well as temporal logic. As an application, similar approach will be investigated for model checking in order to find a way to simplify the complexity of model checking systems.
Modal logic plays an important part in Artificial Intelligence and non-classic mathematical logic. It not only has theoretical roots in temporal logic and knowl-edge reasoning, but also owns applicable root in logic programming. As an expansion of propositional logic, modal logic possesses many particular and unique advantages. For example, there are distinguished types of modalities representing "possibility" and "necessity" together with "future" and "past". The more modalities it owns, the more ability of expression it is provided with. As a result, it seems necessary to extend the quantitative approach to the frame of modal logic, which also comes to one of the investigate assignments for Quantitative Logic. To meet this challenge, the thesis will construct localized truth degree as well as global truth degree for modal formu-lae by considering the locality of Kripke semantics in modal logic. Based on this, a quantitative approach for modal logic will be provided.
Furthermore, as a formalized verification technique, model checking can automat- ically examine all relevant system states to check whether the system model satisfies the desired properties. Since it was proposed in1980s, this breakthrough was the first step towards the automated verification of concurrent programs. Over the last three decades, model checking has received a lot of attention and becomes a subject of rapid-1y growing research community. Since the specification in model checking is typically represented in several temporal logics, this thesis will similarly explore a quantitative approach for temporal logic and attempt to find a way to simplify the complexity of model checking systems based on this.
The main contribution of this thesis is organized into five chapters.
Chapter1provides an overview of several commonly used propositional logic sys-tems with syntax, semantics as well as completeness. Then basic concepts of Quan-titative Logic are recalled, such as truth degree, similarity degree and pseudo-metric for formulae together with the logic metric space.
Chapter2recalls some preliminaries of classical modal logic. Then the Kripke semantics of classical modal logic is extended as lattice-valued ones, which also covers the notion of fuzzy-value ones. Moreover, based on Boolean algebras, a type of lattice-valued modal logic system, named as Boolean-type system B, is proposed. More importantly, this system is proved to be complete, i.e., a modal formula in B is valid if and only if it belongs to the scope of theorems. Lastly, the notion of QMR0algebra is introduced, and underlying logic system, QMR0-type lattice-valued modal logic system QML*, is constructed, whose completeness is ensured as well.
Chapter3defines a certain finite subset of unit interval [0,1] as the valuation field for Kripke semantics of many-value modal logic. In fact, this Kripke semantics is a special case of lattice-valued ones and covers the notion of classical ones. Then by fixing the possible world W and binary relation R, the notion ofn frames is introduced. This notion contributes the construction of localized mappings induced by modal formulae as well as the definition of localized truth degree for modal formulae. More importantly, the localized truth degree satisfies the reduction theorem, i.e., for each modal formula, its localized truth degree equals the one of another formula con-taining no modalities w.r.t the same possible world. Besides, an aggregation method is adopted on localized truth degree, which comes to the notion of global truth degree for modal formulae. It is proved that this global truth degree satisfies the consistency theorem, i.e., for a modal formula containing no modalities, its global truth degree equals the value of truth degree in the propositional sense. Lastly, the concepts of similarity degree and pseudo-metric for modal formulae are proposed based on local- ized and global truth degrees, and the many-value modal logic metric space is also constructed, taking the propositional logic metric space as its subspace.
Chapter4recalls some preliminaries of transition systems as well as linear tempo-ral logic (LTL for short) from model checking theory. Then for a transition system, the notion of satisfactory degree for LTL formulae is defined by adopting a certain kind of evenly distributed probability measure on the set of all its infinite initial paths. This satisfactory degree actually reflects the grade how a transition system satisfies an LTL formula in a quantitative sense. Based on this, the concepts of similarity degree and pseudo-metric are proposed for LTL formulae, and underlying logic metric space is also constructed. Although above notions are set up for transition systems, similar ideas can also be established for the randomized model, i.e., discrete-time Markov chains (DTMC for short). The difference lies in that the transition probability between states in a DTMC is no longer evenly distributed. Lastly, the notions of characters as well as temporal normal form for LTL formulae are introduced. It is pointed out that those LTL formulae with characters can always be checked within finite steps during model checking, even in some cases when the underlying transition system contains infinite states. What is more, the class of LTL formulae with characters can be characterized by full LTLn, the bounded case for LTL
Chapter5presents the concepts of deductive elements as well as maximal con-tractions in Boolean algebras. Then corresponding study of consistency and maximal contractions are considered, and an algorithm principle is proposed to compute all maximal contractions for a consistent set w.r.t. its refutation in Boolean algebras. It is proved that the quotient algebra of the first-order language w.r.t. its provable equivalence relation constitutes a Boolean algebra, and hence the computation of R-contractions for closed formulae in first-order language can be converted into the one in Boolean algebras proposed by this thesis. Furthermore, the notion of basic elements is introduced in Boolean algebras, which contributes to the definitions of clauses as well as Horn clauses transplanted from predicate logic to a special type of Boolean algebras. It is also pointed out that the computation of R-contractions for clauses in classical propositional logic can be converted into the one in Boolean algebras that is generated by basic elements proposed by this thesis.
计量逻辑学的提出旨在将基于概率、积分等工具的数值计算方法引入到以形式推理为特色的数理逻辑中,使原本符号化的推理具备某种灵活性从而扩展其应用范围.这种思想的雏形最初见于从逻辑语义基本概念的程度化入手而在若干命题逻辑系统中所建立的公式真度理论.此后引发了大量的后续研究,包括对逻辑度量空间的拓扑性质与内蕴结构的研究、对逻辑理论的发散度与相容度的研究以及在命题逻辑中建立近似推理的研究等,至今已形成了较为完善和成熟的计量逻辑学理论.如今计量逻辑学的研究对象已从命题逻辑的范围扩展到了表达力更强的模态逻辑、时态逻辑与谓词逻辑的理论之中.若干将计量逻辑学与其他领域相结合的创新性研究也不断涌现,显示出了计量逻辑学的旺盛生命力与广阔的应用前景.本文的研究目的在于探索计量逻辑学与理论计算机科学的新的结合点,将原本在命题逻辑中行之有效的计量化方法向表达力更强的模态逻辑与时态逻辑中推广,并尝试将其应用于以时态逻辑为逻辑背景的模型检验理论之中.
模态逻辑是非经典数理逻辑与人工智能理论相结合的一个重要方面.它不仅是时态逻辑、知识推理的理论基础,又常在应用中作为程序语义描述的工具.作为命题逻辑的模式扩张,模态逻辑具有命题逻辑所不具备的特点.例如模态逻辑中有若干可以表达“可能”、“必然”以及“将来”、“过去”等不同类型概念的模态词,随着模态词的增多,模态逻辑的表达能力也随之增强,此外局部概念的引入以及可能世界之间关系的论述等也使得模态逻辑具有比命题逻辑强得多的表达能力.正是由于这些特点,使得将原本在命题逻辑中行之有效的计量化方法向更为广泛的模态逻辑中推广成为了近几年计量逻辑学的基本研究任务之一.本文将从模态逻辑Kripke语义的局部化特点出发,建立模态公式的局部化真度,继而再利用某种聚合的方法将其推广为模态公式的全局真度,从而在模态逻辑中建立起较为广泛的计量逻辑理论.
另一方面,模型检验是一种形式化的认证方法,可以用来自动地检验某系统的模型是否满足为该系统设定的规范.这一理论已经经历了迅速发展的三十年,受到了人工智能学界的广泛关注,如今已被成功地应用于包括工业、金融、医疗乃至航空航天等重要领域.注意到模型检验理论的逻辑背景是某类特殊的时态逻辑,它们可以看作是模态逻辑的模式扩张.基于这些考虑,本文将进一步把针对模态逻辑的计量化理论向这类时态逻辑中推广,从一个全新的角度建立模型检验中的计量化理论,并讨论如何针对特殊类型的公式来简化模型检验的过程.
全文共分为五章：
第一章首先简要介绍有关命题逻辑的若干预备知识,包括语构理论、语义理论和完备性问题,并介绍几种常用的命题逻辑系统；然后从分析将基本逻辑概念进行程度化的必要性入手,简要介绍计量逻辑学的基本理论,包括公式的真度、公式之间的相似度、公式集上的伪距离以及逻辑度量空间等理论.
第二章首先简要回顾基本模态逻辑的语义理论、语构理论以及完备性问题；其次对基本模态逻辑的Kripke语义进行推广,将基本模型中的赋值域扩充为完备格,从而建立格值模态逻辑的Kripke语义,并证明该语义也将模糊模态逻辑的Kripke语义纳入其框架之下；然后以Boole代数为背景建立Boole型格值模态逻辑系统B,讨论系统B的语义理论与语构理论,并证明完备性定理的成立,即,任一模态公式是系统召中的定理当且仅当它是有效公式,同时指出基本模态逻辑的Kripke模型实际上是本文所提出的Boole型模态模型的特例；最后提出QMR0代数的概念,并以QMR0代数为背景构建QMR0型格值模态逻辑系统QML*讨论系统QML*的语义理论与语构理论,并证明完备性定理的成立,同时指出模糊模态逻辑的Kripke模型实际上是本文提出的QMRo型模态模型的特例.
第三章首先以单位区间[0,1]的有限子集作为赋值域,建立多值模态逻辑的Kripke模型以及相应的语义理论,并指出这种模型一方面是第二章提出的格值模态模型的特例,同时其Kripke语义又将基本模态逻辑的Kripke语义纳入其框架之下;其次采用固定可能世界集W与二元关系R而让赋值映射自由变动的方法建立
第四章首先简要回顾模型检验理论中有关迁移系统以及线性时态逻辑LTL的基本概念；其次在有限迁移系统的全体无穷初始路径之集上引入某种适当的均匀概率测度.并基于该测度考虑迁移系统TS中满足某个LTL公式φ的路径占总路径的比例,从而定义迁移系统TS对于公式φ的满足度,即TS满足φ的程度,同时在此基础上引入LTL公式之间的相似度与伪距离,并构建线性时态逻辑中的度量空间,即LTL逻辑度量空间；然后将以上建立的满足度理论进一步推广至迁移系统的随机化模型,即离散时间马尔可夫链模型,并类似地引入LTL公式的满足度、相似度与伪距离等概念.此时不再要求各个状态之间相互迁移的概率是等值分布的.从而全体无穷初始路径之集上的概率测度也不是均匀分布的；最后引入线性时态逻辑中公式的特征与时态范式等概念,指出存在特征的LTL公式在模型检验中总可以在有限步内判断其有效性,即使相应的迁移系统含有无限多个状态时也是如此,并证明了LTL公式有与其等价的时态范式当且仅当其存在特征,从而一类特殊的LTL公式可以用线性时态逻辑的有界情形LTLn来刻画.
第五章首先在一般Boole代数中引入推演元的概念,并针对Boole代数建立相应的协调集理论;其次在一般Boole代数中引入反驳、极大缩减、极小减集等概念,并分别给出Boole代数中求某个有限不协调集的全体极小不协调子集以及求有限个集合的全体极小选择的算法原理,从而给出求全体极大缩减的方法,同时指出在一阶语言范围内求全体R-缩减的问题可以转化至Boole代数的范围内求解;最后在Boole代数中引入基本元的概念,并将子句及Horn子句等概念移植到一类由基本元生成的特殊Boole代数中,从而在这类特殊Boole代数中给出求子句集的全体极大缩减的算法原理,同时指出经典二值命题逻辑中求子句集(特别是Horn子句集)的全体R-缩减的问题可以转化至由基本元生成的Boole代数范围内求解.
This thesis aims at exploring quantitative approaches for modal logic as well as model checking. As an application, it also attempts to find a way to simplify the complexity of model checking systems.
Quantitative Logic focuses on the combination of formal inference and numerical calculation methods, such as probability and integral, in mathematical logic theory to make it more flexible and applicable. Such research was initially formed by grading basic logical concepts in several propositional logics in order to construct truth degree theory for formulae. Later on, a large number of subsequent research grew up, in-cluding topological and intrinsic structure analysis for logic metric spaces, divergence and consistence degree study for logical theories as well as construction of approxi-mate reasoning in propositional logic. Nowadays, Quantitative Logic not only owns systematic and mature theory within the scope of propositional logl its research sub-jects also cover more expressive logics, such as modal logic, temporal logic and even predicate logic. Besides, various kinds of investigation appear with innovation, which are devoted to combining Quantitative Logic and other related research fields. This thesis aims at exploring a new joint for Quantitative Logic and theoretical computer science. To be more specific, the quantitative approach used in propositional logic will be extended in the range of modal logic as well as temporal logic. As an application, similar approach will be investigated for model checking in order to find a way to simplify the complexity of model checking systems.
Modal logic plays an important part in Artificial Intelligence and non-classic mathematical logic. It not only has theoretical roots in temporal logic and knowl-edge reasoning, but also owns applicable root in logic programming. As an expansion of propositional logic, modal logic possesses many particular and unique advantages. For example, there are distinguished types of modalities representing "possibility" and "necessity" together with "future" and "past". The more modalities it owns, the more ability of expression it is provided with. As a result, it seems necessary to extend the quantitative approach to the frame of modal logic, which also comes to one of the investigate assignments for Quantitative Logic. To meet this challenge, the thesis will construct localized truth degree as well as global truth degree for modal formu-lae by considering the locality of Kripke semantics in modal logic. Based on this, a quantitative approach for modal logic will be provided.
Furthermore, as a formalized verification technique, model checking can automat- ically examine all relevant system states to check whether the system model satisfies the desired properties. Since it was proposed in1980s, this breakthrough was the first step towards the automated verification of concurrent programs. Over the last three decades, model checking has received a lot of attention and becomes a subject of rapid-1y growing research community. Since the specification in model checking is typically represented in several temporal logics, this thesis will similarly explore a quantitative approach for temporal logic and attempt to find a way to simplify the complexity of model checking systems based on this.
The main contribution of this thesis is organized into five chapters.
Chapter1provides an overview of several commonly used propositional logic sys-tems with syntax, semantics as well as completeness. Then basic concepts of Quan-titative Logic are recalled, such as truth degree, similarity degree and pseudo-metric for formulae together with the logic metric space.
Chapter2recalls some preliminaries of classical modal logic. Then the Kripke semantics of classical modal logic is extended as lattice-valued ones, which also covers the notion of fuzzy-value ones. Moreover, based on Boolean algebras, a type of lattice-valued modal logic system, named as Boolean-type system B, is proposed. More importantly, this system is proved to be complete, i.e., a modal formula in B is valid if and only if it belongs to the scope of theorems. Lastly, the notion of QMR0algebra is introduced, and underlying logic system, QMR0-type lattice-valued modal logic system QML*, is constructed, whose completeness is ensured as well.
Chapter3defines a certain finite subset of unit interval [0,1] as the valuation field for Kripke semantics of many-value modal logic. In fact, this Kripke semantics is a special case of lattice-valued ones and covers the notion of classical ones. Then by fixing the possible world W and binary relation R, the notion of
Chapter4recalls some preliminaries of transition systems as well as linear tempo-ral logic (LTL for short) from model checking theory. Then for a transition system, the notion of satisfactory degree for LTL formulae is defined by adopting a certain kind of evenly distributed probability measure on the set of all its infinite initial paths. This satisfactory degree actually reflects the grade how a transition system satisfies an LTL formula in a quantitative sense. Based on this, the concepts of similarity degree and pseudo-metric are proposed for LTL formulae, and underlying logic metric space is also constructed. Although above notions are set up for transition systems, similar ideas can also be established for the randomized model, i.e., discrete-time Markov chains (DTMC for short). The difference lies in that the transition probability between states in a DTMC is no longer evenly distributed. Lastly, the notions of characters as well as temporal normal form for LTL formulae are introduced. It is pointed out that those LTL formulae with characters can always be checked within finite steps during model checking, even in some cases when the underlying transition system contains infinite states. What is more, the class of LTL formulae with characters can be characterized by full LTLn, the bounded case for LTL
Chapter5presents the concepts of deductive elements as well as maximal con-tractions in Boolean algebras. Then corresponding study of consistency and maximal contractions are considered, and an algorithm principle is proposed to compute all maximal contractions for a consistent set w.r.t. its refutation in Boolean algebras. It is proved that the quotient algebra of the first-order language w.r.t. its provable equivalence relation constitutes a Boolean algebra, and hence the computation of R-contractions for closed formulae in first-order language can be converted into the one in Boolean algebras proposed by this thesis. Furthermore, the notion of basic elements is introduced in Boolean algebras, which contributes to the definitions of clauses as well as Horn clauses transplanted from predicate logic to a special type of Boolean algebras. It is also pointed out that the computation of R-contractions for clauses in classical propositional logic can be converted into the one in Boolean algebras that is generated by basic elements proposed by this thesis.
引文
[1]Hamilton A G. Logic for Mathematicians [M]. London:Cambridge University Press, 1978.
[2]Dalen D V. Logic and Structure [M]. New York:Springer-Verlag,1983.
[3]王元元.计算机科学中的逻辑学[M].北京：科学出版社,1989.
[4]胡世华,陆钟万.数理逻辑基础[M].北京：科学出版社,1983.
[5]王国俊.数理逻辑引论与归结原理(第二版)[M].北京：科学出版社,2006.
[6]王国俊.非经典数理逻辑与近似推理(第二版)[M].北京：科学出版社,2008.
[7]Gottwald S. A Treatise on Many-Valued Logics [M]. Baldock:Research Studies Press,2001.
[8]王宪钧.数理逻辑引论[M].北京：北京大学出版社,1982.
[9]陆汝钤.人工智能[M].北京：科学出版社,1988.
[10]石纯一,黄昌宁,王家钦.人工智能原理[M].北京：清华大学出版社,1993.
[11]王永庆.人工智能[M].西安：西安交通大学出版社,1994.
[12]陆钟万.面向计算机科学的数理逻辑[M].北京：科学出版社,1998.
[13]Schuwann J M. Automated Theorem Proving in Software Engineering [M]. Berlin: Springer-Verlag,2001.
[14]Chang C L, Lee R C. Symbolic Logic and Mechanical Theorem Proving [M]. New York:Academic Press,1987.
[15]刘叙华.基于归结方法的自动推理[M].北京：科学出版社,1994.
[16]邱玉辉,张为群.自动推理导论[M].成都：电子科技大学出版社,1992.
[17]Fitting M. First-Order Logic and Automated Theorem Proving [M]. New York: Springer-Verlag,1990.
[18]Lloyd J. Foundations of Logic Programming [M]. New York:Springer-Verlag,1987.
[19]Lobo J, Minker J, Rajasekar A. Foundations of Disjunctive Logic Programming [M]. London:MIT Press,1992.
[20]Mints G. Several formal systems of logic programming [J]. Computers and Artificial Intelligence,1990,9(1):19-41.
[21]陆汝钤,应明生.知识推理的一个模型[J].中国科学E辑,1998,28(4)：363-369.
[22]Fagin R, Halpern J Y, Moses Y, Vardi M Y. Reasoning about Knowledge [M]. London:MIT Press,1996.
[23]Antoniou G. Non-Monotonic Reasoning [M]. Cambridge:MIT Press,1997.
[24]徐宗本,张讲社,郑亚林.计算智能中的仿生学：理论与算法[M].北京：科学出版社,2003.
[25]王国俊.计算智能(第二册)：词语计算与Fuzzy集[M].北京：高等教育出版社,2005.
[26]Zadeh L A. Fuzzy sets [J]. Information and Control,1965,8(3):338-353.
[27]Zadeh L A. Outline of a new approach, to the analysis and decision processes [J]. IEEE Transactions on Systems, Man, and Cybernetics,1973, SMC-3(1):28-44.
[28]王国俊.模糊推理的全蕴涵三Ⅰ算法[J].中国科学E辑,1999,29(1)：43-53.
[29]王国俊.模糊推理的一个新方法[J].模糊系统与数学,1999,13(3)：1-10.
[30]王国俊,宋庆燕.一种新型的三Ⅰ算法及其逻辑基础[J].自然科学进展,2003,13(6)：575-581.
[31]Liu H W, Wang G J. Unified forms of fully implication restriction methods for fuzzy reasoning [J]. Information Sciences,2007,177(3):956-966.
[32]Liu H W, Wang G J. A note on implicators based on binary aggregation operators in interval-valued fuzzy set theory [J]. Fuzzy Sets and Systems,2006,157(24):3231-3236.
[33]Liu H W, Wang G J. A note on the unified forms of triple I method [J]. Computer and Mathematics with Applications,2006,52(10-11):1609-1613.
[34]Liu H W, Wang G J. Multi-criteria decision-making methods based on intuitionistic fuzzy sets [J]. European Journal of Operational Research,2007,179(1):220-233.
[35]Liu H W, Wang G J. Triple I method based on point-wise sustaining degree [J]. Computer and Mathematics with Applications,2008,55(11):2680-2686.
[36]Liu H W, Wang G J. Continuity of triple I methods based on several implications [J]. Computer and Mathematics with Applications,2008,56(8):2079-2087.
[37]刘华文.基于全蕴涵思想的近似推理算法理论[D].西安：陕西师范大学,2008.
[38]李洪兴.模糊控制的插值机理[J].中国科学E辑,1998,28(3)：259-267.
[39]裴道武,傅丽.模糊推理三Ⅰ算法的逻辑基础[J].模糊系统与数学,2004,18(3)：1-10.
[40]裴道武.模糊推理的全蕴涵算法及其还原性[J].数学研究与评论,2004,24(2)：359-368.
[41]裴道武.FMT问题的两种三Ⅰ算法及其还原性[J].模糊系统与数学,2001,15(4)：1-7.
[42]Pei D W. Unified full implication algorithms of fuzzy reasoning [J]. Information Sciences,2008,178(2):520-530.
[43]宋士吉,吴澄.模糊推理的反向三Ⅰ约束算法[J].自然科学进展,2002,12(1)：95-100.
[44]宋士吉,吴澄.模糊推理的反向三Ⅰ算法[J].中国科学,E辑,2002,32(2)：230-246.
[45]彭家寅.基于某些常见蕴涵算子的模糊推理全蕴涵三Ⅰ约束算法[J].自然科学进展,2005,15(5)：539-546.
[46]裴道武.关于模糊逻辑与模糊推理逻辑基础问题的十年研究综述[J].工程数学学报,2004,21(2)：249-258.
[47]Gottwald S. Mathematical fuzzy logics [J]. Bulletin of Symbolic Logic,2008,14(2): 210-239.
[48]吴望名.关于模糊逻辑的一场争论[J].模糊系统与数学,1995,9(2)：1-9.
[49]Yen J. Fuzzy logic:a modern perspective [J]. IEEE Transactions on Knowledge and Data Engineering,1999,11(1):153-165.
[50]Dubois D, Prade H. Possibility theory, probability theory and multiple-valued logics: a clarification [J]. Annals of Mathematics and Artificial Intelligence,2001,32(1-4): 35-66.
[51]Lukasiewicz J. On three-valued logic [J]. Ruch Filozoficzny,1920,5:170-171.
[52]Hajek P. Metamathematics of Fuzzy Logic [M]. Lodon:Kluwer Academic Publisher, 1998.
[53]Reschcr N. Many-Valued Logic [M]. New York:McGraw-Hill,1969.
[54]Gottward S. Fuzzy Sets and Fuzzy Logic [M]. Berlin:Vieweg Verlag,1993.
[55]Rosser J B, Turquette A R. Many-Valued Logics [M]. Amsterdam:North-Holland, 1952.
[56]Pavelka J. On fuzzy logic(Ⅰ) [J]. Z. fur Mathematick Logic u Grundlagen d Mathe-matic,1979,25:45-52.
[57]Pavelka J. On fuzzy logic(Ⅱ) [J]. Z. fur Mathematick Logic u Grundlagen d Math-ematic,1979,25:119-134.
[58]Pavelka J. On fuzzy logic(Ⅲ) [J]. Z. fur Mathematick Logic u Grundlagen d Math-ematic,1979,25:447-464.
[59]Novak V, Perfilieva I, Mockor J. Mathematical Principles of Fuzzy Logic [M]. Boston:Kluwer Academic Publishers,1999.
[60]Hailperin T. Probability logic [J]. Notre Dame Journal of Formal Logic,1984,25(3): 198-212.
[61]Hailperin T. Sentential Probability Logic [M]. London:Associated University Press, 1996.
[62]Nilsson N J. Probabilistic logic [J]. Artificial Intelligence,1986,28(1):71-87.
[63]Nilsson N J. Probabilistic logic revisited [J]. Artificial Intelligence,1993,59(1): 39-42.
[64]王国俊.计量逻辑学(Ⅰ)[J].工程数学学报,2006,23(2)：191-215.
[65]Wang G J, Zhou H J. Introduction to Mathematical Logic and Resolution Principle [M]. Co-published by Oxford:Alpha Science International Limited and Beijing: Science Press,2009.
[66]Wang G J, Zhou H J. Quantitative logic [J]. Information Sciences,2009,179(3): 226-247.
[67]Wang G J. A unified integrated method for evaluating goodness of propositions in several propositional logic systems and its applications [J]. Chinese Journal of Electronics,2012,21(2):195-201.
[68]王国俊.计量逻辑学的基本思想和研究综述[J].模糊系统与数学,2012,26(4)：1-11.
[69]王国俊,傅丽,宋建社.二值命题逻辑中命题的真度理论[J].中国科学E辑,2001,31(11)：998-1008.
[70]王国俊,李壁镜. Lukasiewicz n-值命题逻辑中公式的真度理论和极限定理[J].中国科学E辑,2005,35(6)：561-569.
[71]李骏,黎锁平,夏亚峰.n-值Lukasiewicz逻辑中命题的真度理论[J].数学学报,2004,47(4)：769-780.
[72]李骏,王国俊.Godel n-值命题逻辑中命题的α-真度理论[J].软件学报,2007,18(1)：33-39.
[73]王国俊.适用于多种蕴涵算了的赋值空间上的测度与积分理论[J].中国科学E辑,2001,31(1)：42-50.
[74]Wang G J. A universal theory of measure and integral on valuation spaces with respect to diverse implication operators [J]. Science in China (Ser. E),2000,43(6): 586-594.
[75]李骏,王国俊.逻辑系统Ln*中命题的真度理论[J].中国科学E辑,2006,36(6)：631-643.
[76]Pei D W. On equivalent forms of fuzzy logic systems NM and IMTL [J]. Fuzzy Sets and Systems,2003,138:187-195.
[77]王国俊,宋建社.命题逻辑中的程度化方法[J].电子学报,2006,34(2)：252-257.
[78]王国俊,刘保翠.四种命题逻辑中公式的相对r-重言度理论[J].工程数学学报,2007,24(4)：598-610.
[79]王国俊,高香妮.命题逻辑系统中理论的真度概念及其应用[J].陕西师范大学学报(自然科学版),2009,37(5)：1-6.
[80]王国俊,时慧娴.n值逻辑系统Ln*中广义重言式的计量化研究[J].陕西师范大学学报(自然科学版),2009,37(2)：1-12.
[81]韩邦合,王国俊.二值命题中命题的条件真度理论[J].模糊系统与数学,2007,21(4)：9-15.
[82]张东晓,李立峰.二值命题逻辑公式的语构程度化方法[J].电子学报,2008,36(2)：325-330.
[83]王国俊,王伟,宋建社.命题逻辑中极大和谐理论之集上的拓扑与Cantor三分集[J].陕西师范大学学报(自然科学版),2007,35(2)：1-5.
[84]Wang G J, She Y H. A topological characterization of consistency of logic theories in propositional logic [J]. Mathematical Logic Quarterly,2006,52(5):470-477.
[85]王国俊,折延宏.二值命题逻辑中理论的发散性、相容性及其拓扑刻画[J].数学学报,2007,50(4)：1-10.
[86]周红军.Lukasiewicz模糊命题逻辑中极大相容理论的结构和拓扑刻画[J].陕西师范大学学报(自然科学版),2011,39(1)：1-4.
[87]高菲菲,王国俊.多值命题逻辑中逻辑理论的拓扑刻画[J].模糊系统与数学,2008,22(2)：24-30.
[88]王国俊,周红军.MV-代数的度量化研究及其在Lukasiewicz命题逻辑中的应用[J].数学学报,2009,52(3)：501-514.
[89]胡明娣.逻辑度量空间的内蕴结构的研究[D].西安：陕西师范大学,2011.
[90]胡明娣,王国俊.经典逻辑度量空间中的模2次范整线性空间结构[J].电子学报,2011,39(4)：899-905.
[91]胡明娣,王国俊.经典逻辑度量空间上的反射变换[J].陕西师范大学学报(自然科学版),2009,37(6)：1-4.
[92]Wang G J, Zhang W X. Consistency degrees of finite theories in Lukasiewicz propo-sitional logic [J]. Fuzzy Sets and Systems,2005,149(2):275-284.
[93]Zhou X N, Wang G J. Consistency degrees of theories in some systems of proposi-tional fuzzy logic [J]. Fuzzy Sets and Systems,2005,152(3):321-331.
[94]Zhou H J, Wang G J. A new theory consistency index based on deduction theorems in several logic systems [J]. Fuzzy Sets and Systems,2006,157(3):427-443.
[95]Zhou H J, Wang G J. Generalized consistency degrees of theories w.r.t. formulas in several standard complete logic systems [J]. Fuzzy Sets and Systems,2006,157(15): 2058-2073.
[96]Zhou H J, Wang G J. Consistency degrees of theories and methods of graded reasoning in n-valued R0-logic (NM-logic) [J]. International Journal of Approximate Reasoning,2006,43(2):117-132.
[97]Zhou H J, Wang G J. Characterizations of maximal consistent theories in the formal deductive system L*(NM-logic) and Cantor Space [J]. Fuzzy Sets and Systems, 2007,158(23):2591-2604.
[98]李立峰,王国俊.Lukasiewicz命题集的积分真度、发散度与相容度的分布[J].陕西师范大学学报(自然科学版),2006,34(2)：5-8.
[99]Wang G J, Hui X J, Song J S. The R0-type fuzzy logic metric space and an algorithm for solving fuzzy modus ponens [J]. Computers and Mathematics with Applications, 2008,55(9):1974-1987.
[100]刘华文,王国俊,张诚一.几种逻辑系统中的近似推理理论[J].山东大学学报,2007,42(7)：77-86.
[101]惠小静.计量逻辑学及其随机化研究[D].西安：陕西师范大学,2008.
[102]惠小静,王国俊.经典推理模式的随机化研究及其应用[J].中国科学E辑,2007,37(6)：801-812.
[103]惠小静.三值R0命题逻辑系统的随机化[J].应用数学学报,2009,32(1)：19-27.
[104]惠小静,刘兴祥.三值Godel命题逻辑系统的随机化[J].模糊系统与数学,2009,23(4)：1-7.
[105]李璧镜.模态逻辑中若干问题的研究[D].西安：陕西师范大学,2010.
[106]胡明娣,王国俊.模糊模态逻辑中的永真式与准永真式[J].电子学报,2009,37(11)：2484-2488.
[107]时慧娴,王国俊.多值模态逻辑的计量化方法[J].软件学报,2012,23(12)：3074-3087.
[108]时慧娴,王国俊.基于有限迁移系统的线性时态逻辑的计量化方法[.J].模糊系统与数学,2012,26(5)：30-35.
[109]王国俊.一类一阶逻辑公式中的公理化真度理论及其应用[J].中国科学：信息科学,2012,42(5)：648-662.
[110]周红军.概率计量逻辑学[D].西安：陕西师范大学,2009.
[111]周红军.Borel型概率计量逻辑[J].中国科学：信息科学,2011,41(11)：1328-1342.
[112]Pawlak Z. Rough sets [J]. International Journal of Computer and Information Sci-ence,1982,11:341-356.
[113]Pawlak Z. Rough sets:Theoretical Aspects of Reasoning about Data [M]. Boston: Kluwer Academic Publishers,1991.
[114]折延宏.计量逻辑学与粗糙逻辑的计量化研究[D].西安：陕西师范大学,2010.
[115]She Y H, Wang G J. An axiomatic approach of fuzzy rough sets based on residuated lattices [J]. Computers and Mathematics with Applications,2009,58(1):189-201.
[116]温巧燕,钮心忻,杨义先.现代密码学中的布尔函数[M].北京：科学出版社,2000.
[117]王庆平,王国俊.计量逻辑学中的线性逻辑公式[J].陕西师范大学学报(自然科学版),2012,40(2)：1-5.
[118]王庆平,王国俊.对称逻辑公式在L3*逻辑度量空间中的分布[J].计算机学报,2011,34(1)：105-114.
[119]王庆平.逻辑度量空间中的仿射变换和几类特殊公式的性态研究及其应用[D].西安：陕西师范大学.2012.
[120]马丽娜.模糊推理方法及知识推理的计量化研究[D].西安：陕西师范大学,2011.
[121]Blackburn P, de Rijke M, Venema Y. Modal Logic [M]. New York:Cambridge University Press,2001.
[122]Cresswell M J, Hughes G E. A New Introduction to Modal Logic [M]. London: Routledge,1996.
[123]Fitting M C. Many-valued modal logics [J]. Fundamenta Informaticae,1992,15: 235-254.
[124]Mironov A M. Fuzzy modal logics [J]. Journal of Mathematical Sciences,2005, 128(6):3461-3483.
[125]Ying M S. On standard models of fuzzy modal logics [J]. Fuzzy Sets and Systems, 1988,26(3):357-363.
[126]汪德刚,谷云东,李洪兴.模糊模态命题逻辑及其广义重言式[J].电子学报,2007,35(2)：261-264.
[127]Hajek P. On fuzzy modal logics S5(C) [J]. Fuzzy Sets and Systems,2010,161: 2389-2396.
[128]王国俊,段巧林.模态逻辑中的(n)真度理论与和谐定理[J].中国科学F辑,2009,39(2)：234-245.
[129]Clarke E M, Grumberg O, Pilid D. Model Checking [M]. London:MIT Press,2000.
[130]Baier C, Katoen J P. Principles of Model Checking [M]. London:MIT Press,2008.
[131]Clarke E M, Emerson E A. Design and synthesis of synchronisation skeletons using branching time temporal logic [C]. In:Logic of Programs, LNCS 131,1981,52-71.
[132]Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR [C]. In:Proceedings 5th International Symposium on Programming, LNCS 137, 1982,337-351.
[133]Huth M, Ryan M. Logic in Computer Science-Modelling and Reasoning about Systems (2nd Ed.) [M]. Cambridge:Cambridge University Press,2004.
[134]Jin H, Somenzi F. An Incremental Algorithm to Check Satisfiability for Bounded Model Checking [J]. Electronic Notes in Theoretical Computer Science,2005,119(2): 51-65.
[135]Awedh M, Somenzi F. Termination Criteria for Bounded Model Checking:Exten-sions and Comparison [J]. Electronic Notes in Theoretical Computer Science,2006, 144(1):51-66.
[136]Hajek P. Basic fuzzy logic and BL-algebras [J]. Soft Computing,1998,2(3):124-128.
[137]Cignoli R, Esteva F, Godo L, Torrens A. Basic fuzzy logic is the logic of continuous t-norms and their residua [J]. Soft Computing,2000,4(2):106-112.
[138]Hajek P, Godo L, Esteva F. A complete many-valued logic with product-conjunction [J]. Archive for Mathematical Logic,1996,35(3):191-208.
[139]Esteva F, Godo L. Monoidal t-norm based logic:toward a logic for left-continuous t-norms [J]. Fuzzy Sets and Systems,2001,124(3):271-288.
[140]Jenei S, Montagna F. A proof of standard completeness for Esteva and Godo's logic MTL [J]. Studia Logica,2002,70(2):183-192.
[141]王国俊.模糊命题演算的一种形式演绎系统[J].科学通报,1997,42(10)：1041-1045.
[142]裴道武,王国俊.形式系统L*的完备性及其应用[J].中国科学E辑,2002,32(1)：56-64.
[143]Tuziak R. An axiomatization of the finite-valued Lukasiewicz calculus [J]. Studia Logica,1988,47(1):49-55.
[144]Pogorzeiski W A. The deduction theorem for Lukasiewicz many-valued propositional calculus [J]. Studia Logica,1964,15(1):7-23.
[145]Wang S M, Wang B S, Wang G J. A triangular-norm-based propositional fuzzy logic [J]. Fuzzy Sets and Systems,2003,136(1):55-70.
[146]裴道武,王国俊.形式系统L*的扩张L*n及其完备性[J].中国科学E辑,2003,33(4)：350-356.
[147]裴道武,王三民.形式系统L*(n)的完备性[J].高校应用数学学报A辑,2001,16(3)：253-262.
[148]Davey B A, Priestley H A. Introduction to Lattices and Order [M]. New York: Cambridge University Press,1990.
[149]Erne M. Infinite distributive laws versus local connectedness and compactness prop-erties [J]. Topology and its Applications,2009,156:2054-2069.
[150]王国俊.拓扑分子格理论[M].西安：陕西师范大学出版社,1990.
[151]Halmos P R. Measure Theory [M]. New York:Springer-Verlag.1974.
[152]Billingsley P. Probability and Measure (2nd Ed.) [M]. New York:Wiley,1986.
[153]John E H, Rajeev M, Jeffrey D U. Introduction to Automata Theory, Languages, and Computation (3rd Ed.) [M]. Boston:Addison-Wesley,2007.
[154]Darwixhe A, Pearl J. On the logic of iterated belief revision [J]. Artificial Intelli-gence,1997,89(1):1-29.
[155]Katsuno H, Mendelzon A O. Propositional knowledge base revision and minimal change [J]. Artificial Intelligence,1991,52(3):263-294.
[156]李未.科学发现的逻辑验证[J].中国科学E辑：信息科学,2008,38(12)：2005-2019.
[157]Li W. Mathematical Logic:Foundations For Information Science [M]. Basel: Birkhaeuser Publish,2009.
[158]罗杰,李未.一个在Horn子句中求解极大缩减的算法[J].中国科学：信息科学,2011,41(2)：129-143.
[159]王国俊,时慧娴.格值模态命题逻辑及其完备性[J].中国科学：信息科学,2011,41(1)：66-76.
[160]Shi H X, Wang G J. Lattice-valued modal propositional logic and its completeness [J]. SCIENCE CHINA Information Sciences,2010,53(11):2230-2239.
[161]Shi H X, Wang G J. Maximal contractions in Boolean algebras [J]. SCIENCE CHINA Information Sciences,2012,55(9):2044-2055.
[2]Dalen D V. Logic and Structure [M]. New York:Springer-Verlag,1983.
[3]王元元.计算机科学中的逻辑学[M].北京：科学出版社,1989.
[4]胡世华,陆钟万.数理逻辑基础[M].北京：科学出版社,1983.
[5]王国俊.数理逻辑引论与归结原理(第二版)[M].北京：科学出版社,2006.
[6]王国俊.非经典数理逻辑与近似推理(第二版)[M].北京：科学出版社,2008.
[7]Gottwald S. A Treatise on Many-Valued Logics [M]. Baldock:Research Studies Press,2001.
[8]王宪钧.数理逻辑引论[M].北京：北京大学出版社,1982.
[9]陆汝钤.人工智能[M].北京：科学出版社,1988.
[10]石纯一,黄昌宁,王家钦.人工智能原理[M].北京：清华大学出版社,1993.
[11]王永庆.人工智能[M].西安：西安交通大学出版社,1994.
[12]陆钟万.面向计算机科学的数理逻辑[M].北京：科学出版社,1998.
[13]Schuwann J M. Automated Theorem Proving in Software Engineering [M]. Berlin: Springer-Verlag,2001.
[14]Chang C L, Lee R C. Symbolic Logic and Mechanical Theorem Proving [M]. New York:Academic Press,1987.
[15]刘叙华.基于归结方法的自动推理[M].北京：科学出版社,1994.
[16]邱玉辉,张为群.自动推理导论[M].成都：电子科技大学出版社,1992.
[17]Fitting M. First-Order Logic and Automated Theorem Proving [M]. New York: Springer-Verlag,1990.
[18]Lloyd J. Foundations of Logic Programming [M]. New York:Springer-Verlag,1987.
[19]Lobo J, Minker J, Rajasekar A. Foundations of Disjunctive Logic Programming [M]. London:MIT Press,1992.
[20]Mints G. Several formal systems of logic programming [J]. Computers and Artificial Intelligence,1990,9(1):19-41.
[21]陆汝钤,应明生.知识推理的一个模型[J].中国科学E辑,1998,28(4)：363-369.
[22]Fagin R, Halpern J Y, Moses Y, Vardi M Y. Reasoning about Knowledge [M]. London:MIT Press,1996.
[23]Antoniou G. Non-Monotonic Reasoning [M]. Cambridge:MIT Press,1997.
[24]徐宗本,张讲社,郑亚林.计算智能中的仿生学：理论与算法[M].北京：科学出版社,2003.
[25]王国俊.计算智能(第二册)：词语计算与Fuzzy集[M].北京：高等教育出版社,2005.
[26]Zadeh L A. Fuzzy sets [J]. Information and Control,1965,8(3):338-353.
[27]Zadeh L A. Outline of a new approach, to the analysis and decision processes [J]. IEEE Transactions on Systems, Man, and Cybernetics,1973, SMC-3(1):28-44.
[28]王国俊.模糊推理的全蕴涵三Ⅰ算法[J].中国科学E辑,1999,29(1)：43-53.
[29]王国俊.模糊推理的一个新方法[J].模糊系统与数学,1999,13(3)：1-10.
[30]王国俊,宋庆燕.一种新型的三Ⅰ算法及其逻辑基础[J].自然科学进展,2003,13(6)：575-581.
[31]Liu H W, Wang G J. Unified forms of fully implication restriction methods for fuzzy reasoning [J]. Information Sciences,2007,177(3):956-966.
[32]Liu H W, Wang G J. A note on implicators based on binary aggregation operators in interval-valued fuzzy set theory [J]. Fuzzy Sets and Systems,2006,157(24):3231-3236.
[33]Liu H W, Wang G J. A note on the unified forms of triple I method [J]. Computer and Mathematics with Applications,2006,52(10-11):1609-1613.
[34]Liu H W, Wang G J. Multi-criteria decision-making methods based on intuitionistic fuzzy sets [J]. European Journal of Operational Research,2007,179(1):220-233.
[35]Liu H W, Wang G J. Triple I method based on point-wise sustaining degree [J]. Computer and Mathematics with Applications,2008,55(11):2680-2686.
[36]Liu H W, Wang G J. Continuity of triple I methods based on several implications [J]. Computer and Mathematics with Applications,2008,56(8):2079-2087.
[37]刘华文.基于全蕴涵思想的近似推理算法理论[D].西安：陕西师范大学,2008.
[38]李洪兴.模糊控制的插值机理[J].中国科学E辑,1998,28(3)：259-267.
[39]裴道武,傅丽.模糊推理三Ⅰ算法的逻辑基础[J].模糊系统与数学,2004,18(3)：1-10.
[40]裴道武.模糊推理的全蕴涵算法及其还原性[J].数学研究与评论,2004,24(2)：359-368.
[41]裴道武.FMT问题的两种三Ⅰ算法及其还原性[J].模糊系统与数学,2001,15(4)：1-7.
[42]Pei D W. Unified full implication algorithms of fuzzy reasoning [J]. Information Sciences,2008,178(2):520-530.
[43]宋士吉,吴澄.模糊推理的反向三Ⅰ约束算法[J].自然科学进展,2002,12(1)：95-100.
[44]宋士吉,吴澄.模糊推理的反向三Ⅰ算法[J].中国科学,E辑,2002,32(2)：230-246.
[45]彭家寅.基于某些常见蕴涵算子的模糊推理全蕴涵三Ⅰ约束算法[J].自然科学进展,2005,15(5)：539-546.
[46]裴道武.关于模糊逻辑与模糊推理逻辑基础问题的十年研究综述[J].工程数学学报,2004,21(2)：249-258.
[47]Gottwald S. Mathematical fuzzy logics [J]. Bulletin of Symbolic Logic,2008,14(2): 210-239.
[48]吴望名.关于模糊逻辑的一场争论[J].模糊系统与数学,1995,9(2)：1-9.
[49]Yen J. Fuzzy logic:a modern perspective [J]. IEEE Transactions on Knowledge and Data Engineering,1999,11(1):153-165.
[50]Dubois D, Prade H. Possibility theory, probability theory and multiple-valued logics: a clarification [J]. Annals of Mathematics and Artificial Intelligence,2001,32(1-4): 35-66.
[51]Lukasiewicz J. On three-valued logic [J]. Ruch Filozoficzny,1920,5:170-171.
[52]Hajek P. Metamathematics of Fuzzy Logic [M]. Lodon:Kluwer Academic Publisher, 1998.
[53]Reschcr N. Many-Valued Logic [M]. New York:McGraw-Hill,1969.
[54]Gottward S. Fuzzy Sets and Fuzzy Logic [M]. Berlin:Vieweg Verlag,1993.
[55]Rosser J B, Turquette A R. Many-Valued Logics [M]. Amsterdam:North-Holland, 1952.
[56]Pavelka J. On fuzzy logic(Ⅰ) [J]. Z. fur Mathematick Logic u Grundlagen d Mathe-matic,1979,25:45-52.
[57]Pavelka J. On fuzzy logic(Ⅱ) [J]. Z. fur Mathematick Logic u Grundlagen d Math-ematic,1979,25:119-134.
[58]Pavelka J. On fuzzy logic(Ⅲ) [J]. Z. fur Mathematick Logic u Grundlagen d Math-ematic,1979,25:447-464.
[59]Novak V, Perfilieva I, Mockor J. Mathematical Principles of Fuzzy Logic [M]. Boston:Kluwer Academic Publishers,1999.
[60]Hailperin T. Probability logic [J]. Notre Dame Journal of Formal Logic,1984,25(3): 198-212.
[61]Hailperin T. Sentential Probability Logic [M]. London:Associated University Press, 1996.
[62]Nilsson N J. Probabilistic logic [J]. Artificial Intelligence,1986,28(1):71-87.
[63]Nilsson N J. Probabilistic logic revisited [J]. Artificial Intelligence,1993,59(1): 39-42.
[64]王国俊.计量逻辑学(Ⅰ)[J].工程数学学报,2006,23(2)：191-215.
[65]Wang G J, Zhou H J. Introduction to Mathematical Logic and Resolution Principle [M]. Co-published by Oxford:Alpha Science International Limited and Beijing: Science Press,2009.
[66]Wang G J, Zhou H J. Quantitative logic [J]. Information Sciences,2009,179(3): 226-247.
[67]Wang G J. A unified integrated method for evaluating goodness of propositions in several propositional logic systems and its applications [J]. Chinese Journal of Electronics,2012,21(2):195-201.
[68]王国俊.计量逻辑学的基本思想和研究综述[J].模糊系统与数学,2012,26(4)：1-11.
[69]王国俊,傅丽,宋建社.二值命题逻辑中命题的真度理论[J].中国科学E辑,2001,31(11)：998-1008.
[70]王国俊,李壁镜. Lukasiewicz n-值命题逻辑中公式的真度理论和极限定理[J].中国科学E辑,2005,35(6)：561-569.
[71]李骏,黎锁平,夏亚峰.n-值Lukasiewicz逻辑中命题的真度理论[J].数学学报,2004,47(4)：769-780.
[72]李骏,王国俊.Godel n-值命题逻辑中命题的α-真度理论[J].软件学报,2007,18(1)：33-39.
[73]王国俊.适用于多种蕴涵算了的赋值空间上的测度与积分理论[J].中国科学E辑,2001,31(1)：42-50.
[74]Wang G J. A universal theory of measure and integral on valuation spaces with respect to diverse implication operators [J]. Science in China (Ser. E),2000,43(6): 586-594.
[75]李骏,王国俊.逻辑系统Ln*中命题的真度理论[J].中国科学E辑,2006,36(6)：631-643.
[76]Pei D W. On equivalent forms of fuzzy logic systems NM and IMTL [J]. Fuzzy Sets and Systems,2003,138:187-195.
[77]王国俊,宋建社.命题逻辑中的程度化方法[J].电子学报,2006,34(2)：252-257.
[78]王国俊,刘保翠.四种命题逻辑中公式的相对r-重言度理论[J].工程数学学报,2007,24(4)：598-610.
[79]王国俊,高香妮.命题逻辑系统中理论的真度概念及其应用[J].陕西师范大学学报(自然科学版),2009,37(5)：1-6.
[80]王国俊,时慧娴.n值逻辑系统Ln*中广义重言式的计量化研究[J].陕西师范大学学报(自然科学版),2009,37(2)：1-12.
[81]韩邦合,王国俊.二值命题中命题的条件真度理论[J].模糊系统与数学,2007,21(4)：9-15.
[82]张东晓,李立峰.二值命题逻辑公式的语构程度化方法[J].电子学报,2008,36(2)：325-330.
[83]王国俊,王伟,宋建社.命题逻辑中极大和谐理论之集上的拓扑与Cantor三分集[J].陕西师范大学学报(自然科学版),2007,35(2)：1-5.
[84]Wang G J, She Y H. A topological characterization of consistency of logic theories in propositional logic [J]. Mathematical Logic Quarterly,2006,52(5):470-477.
[85]王国俊,折延宏.二值命题逻辑中理论的发散性、相容性及其拓扑刻画[J].数学学报,2007,50(4)：1-10.
[86]周红军.Lukasiewicz模糊命题逻辑中极大相容理论的结构和拓扑刻画[J].陕西师范大学学报(自然科学版),2011,39(1)：1-4.
[87]高菲菲,王国俊.多值命题逻辑中逻辑理论的拓扑刻画[J].模糊系统与数学,2008,22(2)：24-30.
[88]王国俊,周红军.MV-代数的度量化研究及其在Lukasiewicz命题逻辑中的应用[J].数学学报,2009,52(3)：501-514.
[89]胡明娣.逻辑度量空间的内蕴结构的研究[D].西安：陕西师范大学,2011.
[90]胡明娣,王国俊.经典逻辑度量空间中的模2次范整线性空间结构[J].电子学报,2011,39(4)：899-905.
[91]胡明娣,王国俊.经典逻辑度量空间上的反射变换[J].陕西师范大学学报(自然科学版),2009,37(6)：1-4.
[92]Wang G J, Zhang W X. Consistency degrees of finite theories in Lukasiewicz propo-sitional logic [J]. Fuzzy Sets and Systems,2005,149(2):275-284.
[93]Zhou X N, Wang G J. Consistency degrees of theories in some systems of proposi-tional fuzzy logic [J]. Fuzzy Sets and Systems,2005,152(3):321-331.
[94]Zhou H J, Wang G J. A new theory consistency index based on deduction theorems in several logic systems [J]. Fuzzy Sets and Systems,2006,157(3):427-443.
[95]Zhou H J, Wang G J. Generalized consistency degrees of theories w.r.t. formulas in several standard complete logic systems [J]. Fuzzy Sets and Systems,2006,157(15): 2058-2073.
[96]Zhou H J, Wang G J. Consistency degrees of theories and methods of graded reasoning in n-valued R0-logic (NM-logic) [J]. International Journal of Approximate Reasoning,2006,43(2):117-132.
[97]Zhou H J, Wang G J. Characterizations of maximal consistent theories in the formal deductive system L*(NM-logic) and Cantor Space [J]. Fuzzy Sets and Systems, 2007,158(23):2591-2604.
[98]李立峰,王国俊.Lukasiewicz命题集的积分真度、发散度与相容度的分布[J].陕西师范大学学报(自然科学版),2006,34(2)：5-8.
[99]Wang G J, Hui X J, Song J S. The R0-type fuzzy logic metric space and an algorithm for solving fuzzy modus ponens [J]. Computers and Mathematics with Applications, 2008,55(9):1974-1987.
[100]刘华文,王国俊,张诚一.几种逻辑系统中的近似推理理论[J].山东大学学报,2007,42(7)：77-86.
[101]惠小静.计量逻辑学及其随机化研究[D].西安：陕西师范大学,2008.
[102]惠小静,王国俊.经典推理模式的随机化研究及其应用[J].中国科学E辑,2007,37(6)：801-812.
[103]惠小静.三值R0命题逻辑系统的随机化[J].应用数学学报,2009,32(1)：19-27.
[104]惠小静,刘兴祥.三值Godel命题逻辑系统的随机化[J].模糊系统与数学,2009,23(4)：1-7.
[105]李璧镜.模态逻辑中若干问题的研究[D].西安：陕西师范大学,2010.
[106]胡明娣,王国俊.模糊模态逻辑中的永真式与准永真式[J].电子学报,2009,37(11)：2484-2488.
[107]时慧娴,王国俊.多值模态逻辑的计量化方法[J].软件学报,2012,23(12)：3074-3087.
[108]时慧娴,王国俊.基于有限迁移系统的线性时态逻辑的计量化方法[.J].模糊系统与数学,2012,26(5)：30-35.
[109]王国俊.一类一阶逻辑公式中的公理化真度理论及其应用[J].中国科学：信息科学,2012,42(5)：648-662.
[110]周红军.概率计量逻辑学[D].西安：陕西师范大学,2009.
[111]周红军.Borel型概率计量逻辑[J].中国科学：信息科学,2011,41(11)：1328-1342.
[112]Pawlak Z. Rough sets [J]. International Journal of Computer and Information Sci-ence,1982,11:341-356.
[113]Pawlak Z. Rough sets:Theoretical Aspects of Reasoning about Data [M]. Boston: Kluwer Academic Publishers,1991.
[114]折延宏.计量逻辑学与粗糙逻辑的计量化研究[D].西安：陕西师范大学,2010.
[115]She Y H, Wang G J. An axiomatic approach of fuzzy rough sets based on residuated lattices [J]. Computers and Mathematics with Applications,2009,58(1):189-201.
[116]温巧燕,钮心忻,杨义先.现代密码学中的布尔函数[M].北京：科学出版社,2000.
[117]王庆平,王国俊.计量逻辑学中的线性逻辑公式[J].陕西师范大学学报(自然科学版),2012,40(2)：1-5.
[118]王庆平,王国俊.对称逻辑公式在L3*逻辑度量空间中的分布[J].计算机学报,2011,34(1)：105-114.
[119]王庆平.逻辑度量空间中的仿射变换和几类特殊公式的性态研究及其应用[D].西安：陕西师范大学.2012.
[120]马丽娜.模糊推理方法及知识推理的计量化研究[D].西安：陕西师范大学,2011.
[121]Blackburn P, de Rijke M, Venema Y. Modal Logic [M]. New York:Cambridge University Press,2001.
[122]Cresswell M J, Hughes G E. A New Introduction to Modal Logic [M]. London: Routledge,1996.
[123]Fitting M C. Many-valued modal logics [J]. Fundamenta Informaticae,1992,15: 235-254.
[124]Mironov A M. Fuzzy modal logics [J]. Journal of Mathematical Sciences,2005, 128(6):3461-3483.
[125]Ying M S. On standard models of fuzzy modal logics [J]. Fuzzy Sets and Systems, 1988,26(3):357-363.
[126]汪德刚,谷云东,李洪兴.模糊模态命题逻辑及其广义重言式[J].电子学报,2007,35(2)：261-264.
[127]Hajek P. On fuzzy modal logics S5(C) [J]. Fuzzy Sets and Systems,2010,161: 2389-2396.
[128]王国俊,段巧林.模态逻辑中的(n)真度理论与和谐定理[J].中国科学F辑,2009,39(2)：234-245.
[129]Clarke E M, Grumberg O, Pilid D. Model Checking [M]. London:MIT Press,2000.
[130]Baier C, Katoen J P. Principles of Model Checking [M]. London:MIT Press,2008.
[131]Clarke E M, Emerson E A. Design and synthesis of synchronisation skeletons using branching time temporal logic [C]. In:Logic of Programs, LNCS 131,1981,52-71.
[132]Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR [C]. In:Proceedings 5th International Symposium on Programming, LNCS 137, 1982,337-351.
[133]Huth M, Ryan M. Logic in Computer Science-Modelling and Reasoning about Systems (2nd Ed.) [M]. Cambridge:Cambridge University Press,2004.
[134]Jin H, Somenzi F. An Incremental Algorithm to Check Satisfiability for Bounded Model Checking [J]. Electronic Notes in Theoretical Computer Science,2005,119(2): 51-65.
[135]Awedh M, Somenzi F. Termination Criteria for Bounded Model Checking:Exten-sions and Comparison [J]. Electronic Notes in Theoretical Computer Science,2006, 144(1):51-66.
[136]Hajek P. Basic fuzzy logic and BL-algebras [J]. Soft Computing,1998,2(3):124-128.
[137]Cignoli R, Esteva F, Godo L, Torrens A. Basic fuzzy logic is the logic of continuous t-norms and their residua [J]. Soft Computing,2000,4(2):106-112.
[138]Hajek P, Godo L, Esteva F. A complete many-valued logic with product-conjunction [J]. Archive for Mathematical Logic,1996,35(3):191-208.
[139]Esteva F, Godo L. Monoidal t-norm based logic:toward a logic for left-continuous t-norms [J]. Fuzzy Sets and Systems,2001,124(3):271-288.
[140]Jenei S, Montagna F. A proof of standard completeness for Esteva and Godo's logic MTL [J]. Studia Logica,2002,70(2):183-192.
[141]王国俊.模糊命题演算的一种形式演绎系统[J].科学通报,1997,42(10)：1041-1045.
[142]裴道武,王国俊.形式系统L*的完备性及其应用[J].中国科学E辑,2002,32(1)：56-64.
[143]Tuziak R. An axiomatization of the finite-valued Lukasiewicz calculus [J]. Studia Logica,1988,47(1):49-55.
[144]Pogorzeiski W A. The deduction theorem for Lukasiewicz many-valued propositional calculus [J]. Studia Logica,1964,15(1):7-23.
[145]Wang S M, Wang B S, Wang G J. A triangular-norm-based propositional fuzzy logic [J]. Fuzzy Sets and Systems,2003,136(1):55-70.
[146]裴道武,王国俊.形式系统L*的扩张L*n及其完备性[J].中国科学E辑,2003,33(4)：350-356.
[147]裴道武,王三民.形式系统L*(n)的完备性[J].高校应用数学学报A辑,2001,16(3)：253-262.
[148]Davey B A, Priestley H A. Introduction to Lattices and Order [M]. New York: Cambridge University Press,1990.
[149]Erne M. Infinite distributive laws versus local connectedness and compactness prop-erties [J]. Topology and its Applications,2009,156:2054-2069.
[150]王国俊.拓扑分子格理论[M].西安：陕西师范大学出版社,1990.
[151]Halmos P R. Measure Theory [M]. New York:Springer-Verlag.1974.
[152]Billingsley P. Probability and Measure (2nd Ed.) [M]. New York:Wiley,1986.
[153]John E H, Rajeev M, Jeffrey D U. Introduction to Automata Theory, Languages, and Computation (3rd Ed.) [M]. Boston:Addison-Wesley,2007.
[154]Darwixhe A, Pearl J. On the logic of iterated belief revision [J]. Artificial Intelli-gence,1997,89(1):1-29.
[155]Katsuno H, Mendelzon A O. Propositional knowledge base revision and minimal change [J]. Artificial Intelligence,1991,52(3):263-294.
[156]李未.科学发现的逻辑验证[J].中国科学E辑：信息科学,2008,38(12)：2005-2019.
[157]Li W. Mathematical Logic:Foundations For Information Science [M]. Basel: Birkhaeuser Publish,2009.
[158]罗杰,李未.一个在Horn子句中求解极大缩减的算法[J].中国科学：信息科学,2011,41(2)：129-143.
[159]王国俊,时慧娴.格值模态命题逻辑及其完备性[J].中国科学：信息科学,2011,41(1)：66-76.
[160]Shi H X, Wang G J. Lattice-valued modal propositional logic and its completeness [J]. SCIENCE CHINA Information Sciences,2010,53(11):2230-2239.
[161]Shi H X, Wang G J. Maximal contractions in Boolean algebras [J]. SCIENCE CHINA Information Sciences,2012,55(9):2044-2055.