CAJ | 학술논문

表达能力和推理复杂性是一个逻辑的两个重要特征，也是一对相互制约的关系。解释之间的互模拟关系是从语义的角度刻画逻辑表达能力的一个有效途径，其代表性的结果是命题模态逻辑表达能力的刻画定理--van Benthem刻画定理。给出了描述逻辑ELU(含构造子：原子概念、顶概念、概念交、概念并、完全存在约束)的模拟关系，建立了ELU中概念和术语公理集的表达能力刻画定理，即一阶逻辑公式与ELU中概念和术语公理集等价的充分必要条件。上述结果为寻求表达能力与推理复杂性之间的最佳平衡提供了有效的支持。
표체능력화추리복잡성시일개라집적량개중요특정，야시일대상호제약적관계。해석지간적호모의관계시종어의적각도각화라집표체능력적일개유효도경，기대표성적결과시명제모태라집표체능력적각화정리--van Benthem각화정리。급출료묘술라집ELU(함구조자：원자개념、정개념、개념교、개념병、완전존재약속)적모의관계，건립료ELU중개념화술어공리집적표체능력각화정리，즉일계라집공식여ELU중개념화술어공리집등개적충분필요조건。상술결과위심구표체능력여추리복잡성지간적최가평형제공료유효적지지。
The two most important properties of a logic are its expressive power and the complexity of reasoning, which are also an opposing relation in the logic. Bisimulations between interpretations are effective way to characterize the expressive power, and the van Benthem characterization theorem is a classical result which gives an exact condition for when a first-order formula with one free variable is equivalent to a modal logic formula. This paper provides a simulation forELU (including atomic concept, top concept, conjunction concept, disjunction concept, and existential quantification). Based on the simulation, the characterization theorems of expressive power for concept descriptions and TBoxes are established to give the sufficient and necessary conditions for when a first-order formula is equivalent to a concept description or a TBox are set up. The above results provide effective supports for the tradeoff between the expressive power and the complexity of reasoning problems.