逻辑之间的语义忠实语义满翻译
作者:
基金项目:

国家自然科学基金(60496326, 60573063, 60573064, 60773059, 61103169); 国家高技术研究发展计划(863)(2007AA01Z325)


Faithful and Full Translations Between Logics
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [27]
  • |
  • 相似文献
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    翻译在计算机科学中的一个重要应用是实现一个逻辑与另一个逻辑在表达能力上的比较,以及利用目标逻辑的推理机实现源逻辑的推理.现有逻辑之间的翻译理论和性质没有深入研究逻辑的语义翻译,以及翻译是否保持不可满足性等问题.该文研究了一类同时保持公式的可满足性和不可满足性的翻译——语义忠实语义满翻译,给出了语义忠实语义满翻译的定义,比较了语义忠实语义满翻译与已有文献中翻译定义的区别和联系,讨论了逻辑的可靠性、完备性、可判定性、紧致性、公式的逻辑等价性,以及模型的初等等价性在语义忠实语义满翻译下被保持的问题.运用语义忠实语义满翻译的定义给出了逻辑之间的同义性定义,并证明了同义关系是逻辑之间的一个等价关系.

    Abstract:

    In computer science, an important application of translations includes comparing the expressive power among logics to achieve reasoning tasks of a logic in another defined logic. General properties of translations found in the literature do not give a comprehensive study on semantically translations and the preservation of the unsatisfiability. To preserve the satisfiability and the unsatisfiability of formulas, the definition of faithful and full translation is given, in this paper, and connections between the faithful and full translation, and other definitions of translations in the literature are discussed. Some properties of logics, such as the soundness, the completeness, the decidability, the compactness, the logical equivalence of formulas and the elementary equivalence of models, which are characterized by the existence of faithful and full translations between logics are also studied. By definition of faithful and full translation, the concept of synonymous logics is introduced and the proof for the equivalence of the synonymous relation is also given.

    参考文献
    [1] Hopcroft JE, Ullman JD. Introduction to Automata Theory, Languages and Computation. 3rd ed., New Jersey: Addison-Wesley,2006.
    [2] Sipser M. Introduction to the Theory of Computation. Cambridge: PWS Publishing, 1997.
    [3] Hong JW. Computation: Computability, Similarity and Duality. New York: Pitman, 1986.
    [4] Schmidt RA, Hustadt U. The axiomatic translation principle for modal logic. ACM Trans. on Computational Logic, 2007,8(4):1-55. [doi: 10.1145/1276920.1276921]
    [5] Ohlbach H, Nonnengart A, de Rijke M, Gabbay D. Encoding two-valued nonclassical logics in classical logic. In: Robinson A,Voronkov A, eds. Handbook of Automated Reasoning. Amsterdam: Elsevier, 2001. 1403-1486.
    [6] van Benthem J. Correspondence theory. In: Gabbay D, Guenthner F, eds. Handbook of Philosophical Logic, Vol.2: Extensions ofClassical Logic. Dodrecht: D. Reidel Publishing Company, 1983. 167-247.
    [7] Borgida A. On the relative expressiveness of description logics and predicate logics. Artificial Intelligence, 1996,82(1-2):353-367.[doi: 10.1016/0004-3702(96)00004-5]
    [8] Gradel E. Guarded fragments of first-order logic: A perspective for new description logics? In: Franconi E, De Giacomo G,Macgregor RM, Nutt W, Welty CA, eds. Proc. of the ’98 Int’l Workshop on Description Logics (DL’98). Trento: Istituto Trentinodi Cultura, 1998. 5-8.
    [9] Kurtonina N, de Rijke M. Expressive of concept expression in first-order description logics. Artificial Intelligence, 1999,107(2):303-333. [doi: 10.1016/S0004-3702(98)00109-X]
    [10] Hustadt U, Schmidt RA, Georgieva L. A survey of decidable first-order fragments and description logics. Journal of RelationalMethods in Computer Science, 2004,1(1):251-276.
    [11] de Nivelle H, de Rijke M. Deciding the guarded fragments by resolution. Journal of Symbolic Computation, 2003,35(1):21-58. [doi:10.1016/S0747-7171(02)00092-5]
    [12] Nonnengart A. First-Order modal logic theorem proving and functional simulation. In: Bajcsy R, ed. Proc. of the ’93 Int’l JointConf. on Artificial Intelligence (IJCAI’93). Chambéry: Morgan Kaufmann Publishers, 1993. 80-85.
    [13] Ohlbach H, Schmidt R. Functional translation and second-order frame properties of modal logics. Journal of Logic andComputation, 1997,7(5):581-603. [doi: 10.1093/logcom/7.5.581]
    [14] Lewis D. Counterpart theory and quantified modal logic. Journal of Philosophy, 1968,65(5):113-126. [doi: 10.2307/2024555]
    [15] Forbes G. Counterparts, logic and metaphysics: Reply to Ramachandran. Analysis, 1990,50(3):167-173. [doi: 10.1093/analys/50.3.167]
    [16] Ramachandran M. An alternative translation scheme for counterpart theory. Analysis, 1989,49(3):131-141. [doi: 10.1093/analys/49.3.131]
    [17] Fara M, Williamson T. Counterparts and actuality. Mind, 2005,114(453):1-30. [doi: 10.1093/mind/fzi001]
    [18] Shen YM, Ma Y, Cao CG, Sui YF, Wang J. Logical properties on translations between logics. Chinese Journal of Computers, 2009,32(10):2091-2098 (in Chinese with English abstract).
    [19] Boolos G. On second-order logic. Journal of Philosophy, 1975,72(16):509-527. [doi: 10.2307/2025179]
    [20] Henkin L. Completeness in the theory of types. Journal of Symbolic Logic, 1950,15(2):159-171.
    [21] Kerber M. How to prove higher order theorems in first order logic. In: Mylopoulos J, Reiter R, eds. Proc. of the ’91 Int’l Joint Conf.on Artificial Intelligence (IJCAI’91). San Francisco: Morgan Kaufmann Publishers, 1991. 137-142.
    [22] Kerber M. On the translation of higher-order problems into first-order logic. In: Cohn T, ed. Proc. of the 11th ECAI. Amsterdam,Chichester: John Wiley and Sons, 1994. 145-149.
    [23] Epstein RL. The Semantic Foundations of Logics, Vol.1: Propositional Logics. New York: Oxford University, 1995.
    [24] Prawitz D, Malmnäs PE. A survey of some connections between classical, intuitionistic and minimal logic. In: Schmidt H, et al.,eds. Proc. of the Studies in Logic and the Foundations of Mathematics, Vol. 50. Amsterdam: Elsevier, 1968. 215-229.
    [25] Feitosa HA, D’Ottaviano IML. Conservative translations. Annals of Pure and Applied Logic, 2001,108(1-3):205-227. [doi: 10.1016/S0168-0072(00)00046-4]
    [26] Gabbay D, Kurucz A, Wolter F, Zakharyaschev M. Many-Dimensional Modal Logics: Theory and Applications. Amsterdam:Elsevier, 2003.
    [27] Blackburn P, de Rijke M, Venema Y. Modal Logic. Cambridge: Cambridge University Press, 2001.
    相似文献
引用本文

申宇铭,马越,曹存根,眭跃飞,王驹.逻辑之间的语义忠实语义满翻译.软件学报,2013,24(7):1626-1637

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2010-04-18
  • 最后修改日期:2012-04-16
  • 在线发布日期: 2013-07-02
文章二维码
您是第19920779位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号