摘要
如果考虑逻辑间模型的翻译并且一个逻辑的模型类被翻译为另一个逻辑的模型类的真子类,那么可靠的(the soundness)和完备的(the completeness)翻译可以将不可满足的公式翻译为可满足的公式.针对上述问题,该文提出了语义忠实(the faithfulness)和语义满(the fullness)两条逻辑性质来确保可满足的公式翻译为可满足的公式,不可满足公式翻译为不可满足公式.该文例证了二阶逻辑在标准语义下到一阶逻辑的翻译是语义忠实的但不是语义满的,在Henkin语义下是语义忠实的和语义满的.
Translating one logic into another logic in a satisfiability-preserving way does not im- mediately lead to the preservation of the unsatisfiability, if the models translation is taken into ac- count and the class of models of the first logic is translated to a proper subclass of the class of models of the second logic. In this paper, two logical properties： the faithfulness and the fullness are defined to ensure the preservations of the satisfiability and the unsatisfiability. As an exam- ple, the translation from second-order logic into first-order logic is given. It is shown that under standard semantics, the translation is faithful but not full, whereas it is faithful and full under Henkin semantics.
出处
《计算机学报》
EI
CSCD
北大核心
2009年第10期2091-2098,共8页
Chinese Journal of Computers
基金
国家自然科学基金(60496326
60573063
60573064
60773059)
国家"八六三"高技术研究发展计划项目基金(2007AA01Z325)资助
关键词
翻译
语义忠实翻译
语义满翻译
二阶逻辑
一阶逻辑
translation
faithful translation
full translation
second-order logic
first-order logic
