用户名: 密码: 验证码:
空间凹形区域中拓扑关系模型和形状关系模型的研究
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
关于人工智能的研究方法,时间与空间的表示及推理总是它最重要的组成部分之一。近年来,时空推理日趋成为活跃的研究方向,是人工智能、地理信息系统、机器人导航、图像理解、计算机视觉、时空数据库等领域的重要研究内容之一。
     在众多的空间关系中,对象间的拓扑关系是最基本的,空间拓扑关系模型的研究是空间推理中的热点问题,在定性空间推理中占有极其重要的地位。空间拓扑关系的建模方法主要包括基于逻辑和基于代数两大类,其代表工作分别是Randell等的RCC理论和Egenhofer的交集模型。目前,基于简单对象的空间拓扑关系研究已形成一套较为成熟、完善的理论体系。然而在现实世界中,空间对象不是简单的而是复杂的,传统空间关系模型已难以满足实际应用的需求,基于复杂对象的空间关系形式化模型的研究势必成为今后定性空间推理发展的一个重要趋势。在开发空间关系模型的形式化方法时,一个重要的问题是在表达能力和计算易处理性之间进行权衡。交集模型虽然计算复杂性较低,但其表达力相对有限;RCC形式化模型表达力虽较强,但其推理计算的难度很大。如何建立表达力较强且计算复杂性较低的形式化方法是空间关系建模的重要内容之一。形状是对象最重要的性质,也最难定性描述。传统的空间关系模型多将对象作为统一整体,不考虑其形状特征。随着复杂空间关系建模的发展,定性形状表示日益成为定性空间推理的一个重要方面。
     目前针对复杂对象的空间关系建模研究主要集中在拓扑和方位两方面,复杂空间对象性质的研究主要集中在形状表示方面。本文针对空间中一类特殊的复杂对象(即空间凹形区域),围绕其拓扑关系建模及形状关系表示展开了研究和讨论。分析、总结了当前定性空间推理中复杂对象拓扑关系模型和形状关系模型的相关研究工作。拓扑关系模型方面,为增强传统拓扑模型(以凸形区域为表示基元)的表达力和实用性,针对简单凹形区域(即只包含一个凹处的凹形区域),提出了基于点集理论的拓扑关系模型RCC62,以及基于模态逻辑的拓扑关系模型RCC62*.形状关系模型方面,以基于区域的形状表示为研究主线,为解决Cohn的定性形状表示方法中SameSide谓词存在的问题,给出一种改进的凹处同异侧关系判断方法。
     本文的主要贡献和研究结果如下:
     (1)复杂对象空间关系建模方法
     目前多数空间关系处理方法的研究,只是针对二维空间、简单对象、简单对象(间)单一种类空间关系进行的。但在现实世界中,空间不是二维平面的而是三维立体的,空间对象不是简单的而是复杂的,空间对象间关系不是单一的而是多种并存的,我们称之为复杂空间关系。现有复杂空间关系建模的研究主要包括复杂对象的空间关系建模、空间对象的定性形状表示,三维空间关系模型,多方面空间关系结合推理等。围绕拓扑关系和形状关系的相关研究工作,重点介绍了基于一阶逻辑的拓扑模型、基于模态逻辑的拓扑模型和基于代数方法的拓扑模型,以及定性形状关系模型。
     (2)简单凹形区域拓扑关系模型RCC62
     基于点集拓扑学,对二维空间中简单凹形区域的拓扑关系进行建模,展开了以下研究工作:扩展9-交集矩阵为16-交集矩阵;基于16-交集矩阵,对RCC23进行细化得到RCC62,给出RCC62的概念邻域图和最近拓扑关系图;建立了RCC62的推理系统,推导出RCC62的复合表。RCC62的表达力强于RCC23,对空间关系的刻画更细致、准确。
     (3)拓扑关系模型RCC62*的表示系统
     在RCC62模型的基础上,建立了基于模态逻辑的拓扑关系模型RCC62*的表示系统,具体工作如下:基于S4模态的内部算子以及凸壳算子,给出了16-交集矩阵的模态定义;基于扩展的零阶直觉演算,将RCC62的基本关系转化为由模型约束和蕴含约束构成的模态公式二元组,得到RCC62*的表示系统。RCC62*的表达力不低于RCC62,且其形式化程度要强于RCC62模型。
     (4)拓扑关系模型RCC62*的推理系统
     基于Gentzen的相继式演算推理方法,将拓扑关系的复合推导问题转化为与其对应的模态公式序列的有效性判断问题。分别研究了基于零阶经典演算和零阶直觉演算的RCC8复合关系推导。在此基础上,加入模态凸壳算子,使用凸壳算子的模态特征公式和Hudelmaier规则对模态公式序列的有效性进行判定,从而建立了RCC62*的推理系统。
     (5)空间凹形区域的定性形状表示
     形状是空间对象的重要特征。空间推理中主要使用定性方法描述对象的形状特征。以基于区域的形状表示法为主线,分析了Cohn提出的一种基于连接关系和凸壳概念的分层定性形状表示法;在此基础上,指出Cohn方法中存在的不足之处,并给出一种改进的凹处同异侧关系判断方法,其判断结果更加合理。
     综上所述,本文在空间推理方面的综述,为定性空间推理中复杂对象空间关系建模的进一步研究明确了方向。关于简单凹形区域间拓扑关系模型RCC62的研究,一定程度上完善了RCC23模型,增强了模型的表达力和实用性。结合RCC62模型和模态化的凸壳算子,给出了拓扑关系模型RCC62*的表示系统。基于Gentzen的相继式演算推理方法,建立了RCC62*的推理系统,一定程度上实现了表达力较强、形式化程度较好且计算复杂性较低的空间建模方法。关于定性形状表示方面的研究,弥补了以往空间关系建模中缺少对空间对象本身进行有效表示的不足。
     总之,本文的研究结果对复杂对象拓扑关系建模、空间对象的定性形状表示、基于模态逻辑的定性空间推理以及地理信息系统、空间数据库和空间查询等,具有一定的理论意义和应用价值。
In all the research methods of Artificial Intelligence, the representation and reasoning of time and space is always one of the most important components. In recent years, spatio-temporal reasoning has become the hot researching directions, which makes it the one of the important researches in Geographic Information System, Robotics Navigation, Image Understanding, Computer Vision and Spatio-Temporal Database.
     Among the various spatial relations, the topological relation between spatial objects is the most basic one, which is one of the basic problems in the research of qualitative spatial reasoning. Therefore, research on the model of spatial topological relation became the hot issues in spatial reasoning, and has played a very important role in qualitative spatial reasoning. The methods for modeling spatial topological relation are classified into mainly two kinds, i.e. the logic-based ones and the algebra-based ones, in which the most typical models are Region Connection Calculus (RCC) and intersection model. So far, the research on spatial topological relations of simple objects are formed a mature and sophisticated theory system. However, the spatial objects are not simple but complicated in the real world. It is hard for the traditional topological models to satisfy the requirements of practical applications. Thus, it is necessary to set up the models which can describe the spatial topological relation of complicated objects, which would be one of the most important trends in the future development of spatial reasoning. The major problem in developing a useful formalism for reasoning about spatial information is the trade off between expressive power and computational tractability. Whilst Egenhofer’s representation does allow for certain inferences to be computed effectively, the scope of the theory is limited. On the other hand, although the formalism presented by Randell et al. is very expressive, since it is presented in 1st-order logic, reasoning in the calculus is extremely difficult. How to build a spatial model of topological relation which is both expressive and has a low computational tractability is one of the directions of our research work. Shape is one of the most important features of object, and is hard to describe in a qualitative way. The shape characteristic is not considered in the traditional spatial relation models which take the object as a whole. The qualitative shape representation has become an important aspect in the field of qualitative spatial reasoning as the rapid development of complex spatial relation modeling.
     Researches on spatial relation modeling of complex objects are currently focusing on topological relation models and directional relation models, and the work on property researching of complex spatial objects is mainly focusing on the representation of shape feature. This thesis focuses on the research problems of a special kind of complex objects in space, which is spatial concave region. The topological relation and qualitative shape representation of concave regions are surveyed and discussed. The existing models of topological relation and qualitative shape representation of complex objects are surveyed analyzed. With the topological aspects, in order to enhance the expressiveness and practicability of traditional models which take the convex region as representing elements, the algebraic method based RCC62 model which describes the topological relation between simple concave regions and the logical method based RCC62* model are proposed. With the shape aspect, focusing on the the region-based qualitative shape representation methods, an improved method for distinguishing the SameSide relation of two concavities in a concave region is proposed to resovle the problems existing in Cohn’s method for qualitative shape representation of concave regions.
     The major contributions and research results are as follows:
     (1) The survey of modeling methods on spatial relation of complex objects.
     Most of the existing methods in spatial relation modeling are limited for describing simple objects, the single spatial relation between simple objects in 2D space. However, the world we lived in is 3D space, the spatial object in it is also complex and there are more than one spatial relation exists in the real world, which we called complex spatial relation. The existing researches on complex spatial relation modeling mainly include the topological relation models of complex objects, the qualitative shape representation of spatial object, the 3D spatial relation models, and the reasoning of combined spatial relation. Focusing on the relative research work on topological relation and shape relation, the first-order based topological models, the modal logic based topological modesl, the algebraic based topological models and the qualitative shape representation models are surveyed and analyzed.
     (2) RCC62 model for representing and reasoning of simple concave regions
     Based on the point set topology theory, the modeling for topological relation of simple concave regions is conducting which includes the following research work: based on 16-intersection matrix, the RCC23 are refined to RCC62. The Conceptual Neighborhood Graph and the Closest Topological Relation Graph of RCC62 are given; reasoning formalism for RCC62 is presented, from which the composition table of RCC62 can derived. There are 39 new relations in RCC62, which is more expressive than RCC23, in which the description for spatial relation is more accurate.
     (3) The representing system of topological relation model RCC62*
     On the basis of RCC62 model, the representing system of topological relation formal model is proposed in a modal way, which includes the following research work: based on the interior operator of S4 modal logic and Bennett’s modal explanation of convex hull operator, the modal definition of 16-intersection matrix is given; based on the extended intuitionistic 0-order calculus, the basic relations of RCC62 is transformed to a two-tuple structure which composed of both model constraint and entailment constraint, from which the representing system of RCC62* model is derived. The expressiveness of RCC62* is the same as RCC62, yet RCC62* has a more formal representation structure than RCC62.
     (4) The reasoning system of topological relation model RCC62*
     Several usual reasoning methods in modal logics are introduced, which include tabuleaux based, resolution based, translation based and sequent calculus based reasoning methods. Based on Gentzen’s sequent calculus reasoning method, the reasoning procedure of spatial relation is translated into the validity determination problem of the corresponding sequent of modal formula. The reasoning of spatial relations which are instances of the RCC8 relation set are analysed respectively in a 0-order classic calculus and a 0-order intuitionistic calculus. The modal convex-hull operator is then introduced and the validity testing for certain sequent of modal formula is implemented based on the modal schema of convex-hull operator and Hudelmaier’s proof rules. The reasoning system of RCC62 is then established in a modal way.
     (5) The qualitative shape representation of spatial concave regions
     Shape characteristic is one of the important features of a spatial object. The qualitative representation method is adopted for characterizing the shape features of objects in spatial reasoning. Among the region-based methods for qualitative shape representation, Cohn’s hierarchical method base on connection and convex hull is analyzed; in order to solve the problems existing in Cohn’s SameSide predicate, an improved method of qualitative shape representation for SameSide distionction of concavities is presented. The results derived using our improved method is more reasonable.
     The survey of research contributions in spatial reasoning, direct the further research on spatial relation models of complex object in qualitative spatial reasoning. The research work on topological relations modeling between simple concave regions, have a refinement of the RCC23 model, thus both the expressiveness and practicality of the original model are inhanced. Combined with RCC62 model and Bennett’s modal explanation of convex hull operator, the representing system of topological relation model RCC62* is proposed. The reasoning system of RCC62* is also established based on Gentzen’s sequent calculus reasoning method. The research work on modeling spatial topological relation in a modal way has the advantage of both expressive and of lower computational complexity. Research on qualitative shape representation makes up the deficiency of lacking effective description of the spatial object itself.
     In a word, the study results of this thesis are of both theoretical and practical benefit to further researches on modeling topological spatial relation of complex objects, qualitative shape representation of spatial object, modal logic based qualitative spatial reasoning, Geographic Information System and Spatial Database.
引文
[1] Kuipers, B. J. Modelling spatial knowledge [J]. Cognitive Science, 1978, 2:129-153.
    [2] A.G.Cohn, S.M. Hazarika. Qualitative Spatial Representation and Reasoning: An Overview [J]. Fundamental Informatics, 2001, 46(1-2):1-29.
    [3] Suh-Yin Lee, Fang-Jung Hsu. Spatial Reasoning and Similarity Retrieval of Images using 2D C-Sstring Knowledge Representation [J]. Pattern Recognition, 1992, 25(3):305-318.
    [4]欧阳继红,刘亚彬,刘大有,欧阳丹彤,虞强源.空间推理及其研究现状[C].第六届中国人工智能联合学术会议论文集,清华大学出版社, 2001: 23-28.
    [5]欧阳继红.时空推理中一些问题的研究[D].长春:吉林大学计算机科学与技术学院, 2005.
    [6]曹菡,陈军,杜道生.空间目标方向关系的定性扩展描述[J].测绘学报, 2001, 30(2): 162-167.
    [7]陈军,赵仁亮. GIS空间关系的基本问题与研究进展[J].测绘学报, 1999, 28(2): 95-102.
    [8] Randell, D.A., Cui, Z., Cohn, A.G. A Spatial Logic based on Regions and Connection [C]. In: Nebel, B.Rich, C. Swartout, W.R. eds. Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning. San Francisco: Morgan Kaufmann Publishers, 1992.
    [9] Max J. Egenhofer, Robert D. Franzosa. Point-set Topological Spatial Relations [J]. International Journal of Geographical Information Science, 1991, 2: 161-174.
    [10] S.Y. Lee, F.J. Hsu. 2D C-string: a new spatial knowledge representation for image database system [J]. Pattern Recognition, 1990, 23: 1077-1087.
    [11] F.P. Coenen, P. Visser. A General Ontology for Spatial Reasoning in Research and Development in Expert Systems XV [C]. R. Miles, M. Moulton, M. Bramer, Eds: Proceedings of ES-98, Berlin: Springer-Verlag, 1998: 44-57.
    [12] Kainz W, Egenhofer M J, Greasley I. Modeling spatial relations and operations with partially orders [J]. Geographic Information Systems,1993, 7(3): 215-229.
    [13]陈娟.空间方位关系模型及多方面空间关系结合推理的研究[D].长春:吉林大学计算机科学与技术学院, 2007.
    [14]谢琦,刘大有,虞强源,陈娟.定性方向关系模型研究进展[J].计算机科学, 2006, 33: 5-9.
    [15] Andrew U Frank. Qualitative spatial reasoning about cardinal directions [C]. In the 7th Austrian Conference on Artificial Intelligence, 1991: 157-167.
    [16] Christian Freksa. Using orientation information for qualitative spatial reasoning [C]. In Theories and methods of spatio-temporal reasoning in geographic space, LNCS 639, Berlin, Heidelberg,New York: Springer-Verlag, 1992.
    [17] Philippe Balbiani, Jean-Francois Condotta, Luis Farinas del Cerro. A new Tractable Subclass of the Rectangle Algebra [C]. In IJCAI-99, 1999: 442-447.
    [18] Roop Goyal, Max J Egenhofer. Cardinal directions between extended spatial objects [J]. IEEE Transactions on Knowledge and Data Engineering, 2000.
    [19] Spiros Skiadopoulos, Manolis Koubarakis. Composing cardinal direction relations [J]. Artificial Intelligence, 2004, 152: 143-171.
    [20] Leyton M. A process grammar for shape [J]. Artificial Intelligence, 1988: 34.
    [21] Cohn AG. A hierarchical representation of qualitative shape based on connection and convexity [C]. In: Proc of COSIT-95, Semmering, 1995.
    [22] Rohrig, R. A Theory for Qualitative Spatial Reasoning Based on Order Relations [C]. Proceedings of the 12th National Conference on Artificial Intelligence, AAAI-94, 1994, 2: 1418-1423.
    [23] Bennett, B. Spatial Reasoning with Propositional Logics [C]. In: Doyle J, Sandewall E, Torasso P eds. Principles of Knowledge Representation and Reasoning: Proceedings of the 4th International Conference (KR-94), San Francisco: Morgan Kaufmann Publishers, 1994: 51-62.
    [24] Roy, A.J, Stell, J.G. Spatial relations between indeterminate regions [J]. International Journal of Approximate Reasoning, 2001, 27(3): 205-234.
    [25]刘亚彬,刘大有,王飞.定性空间表示与定性空间的研究与发展[J].计算机科学, 2003, 30(3): 65-67.
    [26] B. Clarke. A calculus of individuals based on’connection’[J]. Notre Dame Journal of Formal Logic, 1981, 22(3):204-218.
    [27] B.L. Clarke. Individuals and points [J]. Notre Dame Journal of Formal Logic, 1985, 26(1):61-75.
    [28] Cohn AG. A hierarchical representation of qualitative shape based on connection and convexity [C]. Proc of the Int Conf on Spatial Information Theory: A Theoretical Basis for GIS. Berlin / Heidelberg: Springer, 1995: 311-326.
    [29] Bennett B, Cohn A G. Multi-dimensional multi-modal logics as a framework for spatio-temporal reasoning [C]. In: Proc of the `Hot Topics in Spatio-Temporal Reasoning' workshop, IJCAI-99, Stockholm, 1999.
    [30] Freksa C. Temporal reasoning based on semi-intervals [J]. Artificial Intelligence, 1992, 54: 199-227.
    [31] Cohn AG, Randell DA, Cui Z, Bennett B. Qualitative Spatial Reasoning and Representation [C]. In: Qualitative Reasoning and Decision Technologies, CIMNE, Barcelona, 1993: 513-522.
    [32] Cohn AG, Bennett B, Gooday J, Gotts NM. Qualitative spatial representation and reasoning with the region connection calculus [J]. GeoInformatica, 1997, 1(1): 1-44.
    [33] S. Kripke. A completeness theorem in modal logic [J]. Journal of Symbolic Logic, 1959, 24: 1-14.
    [34] B F Chellas. Modal Logic: An Introduction [M]. Cambridge University Press, 1980.
    [35] E J Lemmon. Algebraic semantics for modal logics I [J]. Journal of Symbolic Logic, 1966, 31:46-65.
    [36] A. Tarski, J.C.C. McKinsey. Some theorems about the sentential calculi of Lewis and Heyting [J]. Journal of Symbolic Logic, 1948, 13: 1-15.
    [37] E J Lemmon. Algebraic semantics for modal logics II [J]. Journal of Symbolic Logic, 1966, 31: 191-218.
    [38] R. Goldblatt. Metamathematics of modal logic [M]. In Metamathematics of Modality, chapter 1, CLSI Publications, 1993.
    [39] B. Bennett. Spatial reasoning with propositional logics [C]. In J Doyle, E Sandewall, P Torasso, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the 4th International Conference (KR-94), San Francisco, CA: Morgan Kaufmann, 1994.
    [40] A. Tarski. Foundations of the geometry of solids [M]. In Logic, Semantics, Mctamathcmatics, chapter 2, Oxford Clarendon Press, 1956.
    [41] K. Kuratowski. Introduction to Set Theory and Toplolgy [M]. Pergamon Press, 2nd edition, 1972.
    [42] Güting RH. Geo-relational algebra: a model and query language for geometric database systems [C]. In: Advances in Database Technology, EDBT-98, LNCS 303, Berlin: Springer-Verlag, 1988: 506-527.
    [43] Egenhofer MJ, Herring J. Categorizing binary topological relationships between regions, lines and points in geographical database [R]. Technical Report. Department of Surveying Engeering, University of Maine, 1991.
    [44] S. Zlatanova. 3D Gis for Urban Development [D]. Amsterdam: ITC, 2000.
    [45] T. Behr, M. Schneider. Topological Relationships of Complex Points and Complex Regions [C]. In: H.S. Kunii, S. Jajodia, A. Solvberg (eds.): The 20th Int. Conf. on Conceptual Modeling, LNCS 2224, Berlin Heidelberg: Springer-Verlag, 2004: 56-69.
    [46] M. Schneider, T. Behr. Topological Relationships between Complex Spatial Objects [J]. ACM Transactions on Database Systems, 2006, 31(1): 39-81.
    [47] S. Li. A Complete Classifcation of Topological Relations Using 9-Intersection Method [J]. International Journal of Geographical Information Science (IJGIS), 2006, 20: 589-610.
    [48] J.H. OuYang, Q. Fu, D.Y. Liu. A Model for Representing Topological Relations between Simple Concave Regions [C]. Y. Shi, G.D.v. Albada, J. Dongarra, P.M.A. Sloot (Eds.): The 7th International Conference of Computational Science (ICCS-2007), Proceedings, Part I, LNCS 4487. Beijing, China: Springer Berlin / Heidelberg, 2007: 160-167.
    [49] M. Egenhofer and M. Vasardani, Spatial Reasoning with a Hole [C]. Conference on Spatial Information Theory (COSIT -07), Springer, 2007: 303-320.
    [50] M. McKenney, A. Pauly, R. Praing, M. Schneider. Local Topological Relationships for Complex Regions [C]. 10th Int. Symp. on Spatial and Temporal Databases (SSTD), LNCS 4605, Springer-Verlag, 2007: 203-220.
    [51]欧阳继红,富倩,刘大有.简单凹形区域间空间关系的一种表示及推理模型[J].电子学报, 2009, 37(8): 1830-1836.
    [52] Q. Fu, J.H. OuYang, D.Y. Liu. A Modal Representation of RCC62 [C]. The 5th International Conference of Computer Science and Convergence Information Technology (ICCIT-2010), Nov.30-Dec.2, Seoul, Korea, 2010. (已录用)
    [53] Leyton M. A process grammar for shape. Artificial Intelligence. 1988, 34.
    [54] B. Gottfried. Tripartite Line Tracks [C]. In: K. Wojciechowski (eds.): International Conference on Computer Vision and Graphics, Proc. of ICCVG-2002, Zakopane, Poland, 2002: 288-293.
    [55] B. Gottfried. Tripartite Line Tracks, Qualitative Curvature Information [C]. In: W. Kuhn, M.F. Worboys, S. Timpf (eds.): Spatial Information Theory: Foundations of Geographic Information Science, Pro. of COSIT, LNCS 2825, Berlin Heidelberg: Springer-Verlag, 2003: 101-117.
    [56] B. Gottfried. Global Feature Schemes for Qualitative Shape Descriptions [C]. In: H. W. Guesgen, Ch. Freksa, G. Ligozat (Eds.), IJCAI-05, Workshop notes on spatial and temporal reasoning. Edinburgh, Scotland, 2005.
    [57] B. Gottfried. Characterizing Meanders Qualitatively [C]. In: M. Raubal, H. Miller, A. Frank, M. Goodchild: Geographic Information Science, The 4th Int. Conf. of GIScience, LNCS 4197, Berlin Heidelberg: Springer, 2006: 112-127.
    [58] A. Schuldt, B. Gottfried, O. Herzog. Retrieving Shapes Efficiently by a Qualitative Shape Descriptor: The Scope Histogram [C]. The 5th Int. Conf. of Image and Video Retrieval (CIVR), LNCS 4071, Springer, 2006: 261-270.
    [59] A. Schuldt, B. Gottfried, O. Herzog. A Compact Shape Representation for Linear Geographical Objects: The Scope Histogram [C]. The 14th ACM Int. Symposium on Advances in Geographic Information Systems (ACM GIS), Arlington, VA, USA, 2006.
    [60] B. Gottfried, Arne Schuldt, Otthein Herzog. Extent, Extremum, and Curvature: Qualitative Numeric Features for Efficient Shape Retrieval [C]. 30th Annual German Conference onArtificial Intelligence (KI-2006), Osnabrück, Germany, 10-13 September 2007.
    [61] E. Staffetti, A. Grau, F. Serratosa, A. Sanfeliu. Object and image indexing based on Region Connection Calculus and Oriented Matroid Theory [J]. Discrete Applied Mathematics, 2005, 147(2-3): 345-361.
    [62] Egenhofer MJ, Al-Taha K. Reasoning about gradual changes of topological relationships [C]. Frank A, Theories and models of spatio-temporal reasoning in geographic space, Berlin / Heidelberg: Springer, 1992: 196-219.
    [63] El-Geresy BA, Abdelmoty AI. Order in space: a general formalism for spatial reasoning [J]. International Journal on Artificial Intelligence Tools, 1997, 6(4):423-450.
    [64]吴瑕.基于扩展规则的定理证明的研究[D].长春:吉林大学计算机科学与技术学院, 2006.
    [65] J. A. Robinson. A machine oriented logic based on the resolution principle [J]. Computer Machine, 1965, 12: 23-41.
    [66] G. Mints. Gentzen-Type systems and resolution rules, PartⅠ: propositional logic [C]. In: Proc. of International Conference on Computer Logic, Tallinn, USSR, 1990, 417: 198-231.
    [67] P. Enjalbert, L. Farinas del Cerro. Modal resolution in clauset form [J]. Theoretic Computer Science, 1989, 65: 1-34.
    [68] Y. Auffray, P. Enjalbert, J. Herbrand. Strategies for modal resolution: results and problems [J]. Journal of Automated Reasoning, 1990, 6(1): 1-38.
    [69]孙吉贵,刘叙华.模态归结弱包含删除策略[J].计算机学报, 1994, 17(5): 321-329.
    [70]孙吉贵,刘叙华.标记模态归结推理[J].软件学报, 1996, 7(增刊): 156-162.
    [71]孙吉贵,刘叙华. Cialdea一阶模态归结系统的不完备性及其改进[J].计算机学报, 1995, 18(6): 401-408.
    [72]孙吉贵,刘瑞胜,陈荣.标记模态归结推理的推广[J].计算机学报, 1999, 2(22): 113-119.
    [73] C. Areces, H. de Nivelle, M. de Rijke. Prefixed Resolution: A resolution method for modal and description logics [C]. In: Proc. of 16th International Conference on Automated Deduction (CADE-1999), Trento, Italy, 1999: 187-201.
    [74] C. Areces, H. de Nivelle, M. de Rijke. Resolution in modal, description and hybrid logic [J]. Journal of Logic and Computation, 2001, 11(5): 717-736.
    [75] C. Areces, J. Heguidabehere. HyLoRes: A hybrid logic prover based on direct resolution [C]. In:Proc. of 4th Workshop on Advances in Modal Logic (AIML-2002), Toulouse, France, 2002.
    [76] M. Fisher. A resolution method for temporal logic [C]. In: Proc. of 12th International Joint Conference on Artificial Intelligence (IJCAI-1991), Sydney, Australia, 1991: 99-104.
    [77] M. Fisher, C. Dixon, M. Peim. Clausal temporal resolution [J]. ACM Transactions onComputational Logic, 2001, 2(1): 12-56.
    [78] C. Dixon, M. Fisher, M. Wooldridge. Resolution for temporal logics of knowledge [J]. Journal of Logic and Computation, 1998, 8(3): 345-372.
    [79] A. Degtyarev, M. Fisher, B. Konev. Monodic temporal resolution [C]. In: Proc. of 19th International Conference on Automated Deduction (CADE-2003), Miami, USA, 2003, 2741: 397-411.
    [80] B. Konev, A. Degtyarev. Towards the implementation of first-order temporal resolution: the finite domain case [C]. In: Proc. of 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL-2003), Queensland, Australia, 2003: 72-82.
    [81] B. Konev, A. Degtyarev, M. Fisher. Handling Equality in Monodic Temporal Resolution [C]. In: Proc. of the Logic for Programming and Automated Reasoning (LPAR-2003), Almaty, Kazakhstan, 2003, 2850: 214-228.
    [82] J. van Benthem. Modal correspondence theory [D]. University of Amsterdam, Holand, 1976.
    [83] H. J. Ohlbach. Semantics-based translation methods for modal logics [J]. Journal of Logic and Computation, 1991, 1(5): 691-746.
    [84] R. A. Schmidt. Optimized modal translation and resolution [D]. Universit?t des Saarlandes, 1997.
    [85] A. Nonnecgart. A resolution-based calculus for temporal logics [D]. Universit?t des Saarlandes, Germany, 1995.
    [86] C. Christian, G. Fermüller, A. Leitsch, U. Hustadt, T. Tammet. Resolution decision procedures [M]. In: A. Robinson, A. Voronkov(eds.), Handbook of Automated Reasoning, Elsevier Science Publishers, 2001: 1791-1849.
    [87] U. Hustadt, R.A. Schmidt. Issues of decidability for description logics in the framework of resolution [C]. In: Proc. of Automated Deduction in Classical and Non-Classical Logics (FTP-1998), Vienna, Austria, 1998: 191-205.
    [88] U. Hustadt, R.A. Schmidt. Using resolution for testing modal satisfiability and building models [J]. SAT 2000 Special Issue of Journal of Automated Reasoning, 2000: 459-483.
    [89] G. Gentzen. Untersuchungen uber das logische Schliessen. Mathematische Zeitschrift, 1935, 39: 176-210, 405-431.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700