G-逻辑及其归结推理

该文提出了一种粒-逻辑，简记为G-逻辑，并构造了这种逻辑的近似推理系统，定义了G-公式、G-子句和G-文字，提出了这种逻辑的G-归结方法．G-归结的完备性定理也被证明了．这种逻辑公式的结构是有序二元对，第一元是断言；第二元是对应于这个断言的可定义集或不可定义域集的近似集．这种逻辑是定义在信息系统IS=(U，A)上，所以其公式中的个体变量被赋予U上的实体．公式中的命题或谓词被解释为属性集A上的属性，因此命题或谓词的意义集是U上的一个子集、属性及其意义集一起构成的二元对，被称做一个基本粒(granule)．而这种基本粒被当做这种逻辑中的一个G-原子，用G逻辑联结词组合这些G-原子便得到这种逻辑中的G-公式．公式的可满足性是其相应断言的意义集不空．当这种公式的定义域集不可定义时，则可将它移到其定义域集的Rough下和上近似集上去讨论．G-逻辑的提出为经典逻辑的应用开辟了新途径，也为处理非规范知识提供了较好的理论工具．G-逻辑的运算涉及整体到局部的分解和局部到整体的合并，以此提供了AI中问题求解的新思路．G-逻辑也是Rough逻辑的新扩充，其真值概念及其运算都不同于经典逻辑，也不同于其它非标准逻辑．这种逻辑中的演算既是逻辑的，又是集合论的．于是当处理真值及其运算时适合使用逻辑方法；而处理归结中的文字合一时可用集合论方法，这样可避免复杂的文字合一计算．最后，用实例说明了这种逻辑的G-归结方法的可行性和有效性，并给出了G-逻辑中机器定理证明的相关定理，讨论了G-归结反演的完备性和完全性．

G-Logic and Its Resolution Reasoning

This paper proposes a granular logic, in brief written by G -logic, constructs the systems of approximate reasoning in the G -logic. It defines the G -formula, G -clause and G -literal, and to give the methods of G -resolution in the logic. The soundness theorem of the G -resolution is also proved. The logical formulas are an ordered binary pair, the first element is an assertion and the second is a definable domain or approximations of undefinable domain corresponding to the assertion. The logic is defined on information system IS=(U,A). So the assignment to individual variables in the formulas is an entity on U. The propositions or predicates in the formula are interpreted as attributes in A, hence meaning set of proposition or predicate is a subset on U, the pair of constructed by attribute and its meaning set together is called as an elementary granule. And the elementary granules are used as G -atoms in the logic. A G -formula in the logic is combined by the G -atoms with granular logical connectives. Satisfibility of the logical formula is that meaning set corresponding to it is not empty. If the domain of a formula in the logic is undefinable then the formula is discussed in the rough lower and upper approximations of the domain. The study of G -logic opens a new path for applications of classical logic. G -logic provides a better theoretical tool for treating of irregular knowledge. The operation of G -logic involves the decomposing of global and amalgamating of locals, thus it provides a new idea for solving -problem in AI. G -logic is a new generalization of Rough Logic, truth concept and its operations of the logic is different from classical logic and all non -standard logic. The logic is both logic and set theory. Thus it may use the logical methods when treating truth values and its operations, and it may also avoid the calculation of literal unifier with set theory approach in the G -resolution. Finally, the validity and feasibility of the G -resolution are illustrated with real examples. The related theorems in machine theorem proving are proposed and the soundness and completeness of the theorem for G -resolution refutation are discussed.