###
Journal of Software:2013.24(7):1626-1637

逻辑之间的语义忠实语义满翻译
申宇铭,马越,曹存根,眭跃飞,王驹
(中国科学院 计算技术研究所 智能信息处理重点实验室, 北京 100190;中国科学院 研究生院, 北京 100049;广西师范大学 计算机科学与信息工程学院, 广西 桂林 541004)
Faithful and Full Translations Between Logics
SHEN Yu-Ming,MA Yue,CAO Cun-Gen,SUI Yue-Fei,WANG Ju
(Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, The Chinese Academy of Sciences, Beijing 100190, China;Graduate University, The Chinese Academy of Sciences, Beijing 100049, China;School of Computer Science and Information Engineering, Guangxi Normal University, Guilin 541004, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 2212   Download 2116
Received:April 18, 2010    Revised:April 16, 2012
> 中文摘要: 翻译在计算机科学中的一个重要应用是实现一个逻辑与另一个逻辑在表达能力上的比较,以及利用目标逻辑的推理机实现源逻辑的推理.现有逻辑之间的翻译理论和性质没有深入研究逻辑的语义翻译,以及翻译是否保持不可满足性等问题.该文研究了一类同时保持公式的可满足性和不可满足性的翻译——语义忠实语义满翻译,给出了语义忠实语义满翻译的定义,比较了语义忠实语义满翻译与已有文献中翻译定义的区别和联系,讨论了逻辑的可靠性、完备性、可判定性、紧致性、公式的逻辑等价性,以及模型的初等等价性在语义忠实语义满翻译下被保持的问题.运用语义忠实语义满翻译的定义给出了逻辑之间的同义性定义,并证明了同义关系是逻辑之间的一个等价关系.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(60496326, 60573063, 60573064, 60773059, 61103169); 国家高技术研究发展计划(863)(2007AA01Z325) 国家自然科学基金(60496326, 60573063, 60573064, 60773059, 61103169); 国家高技术研究发展计划(863)(2007AA01Z325)
Foundation items:
Reference text:

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

SHEN Yu-Ming,MA Yue,CAO Cun-Gen,SUI Yue-Fei,WANG Ju.Faithful and Full Translations Between Logics.Journal of Software,2013,24(7):1626-1637