本文提出了一种新的定义UML形式化语义的方法。我们将建模语言的语义区分为描述语义和功能语义两个方面。描述语义定义哪些系统满足模型，功能语义定义模型中的基本概念。本文用一阶逻辑定义了UML的类图、交互图和状态图的描述语义，并介绍我们实现的将UML模型转换成逻辑系统的软件工具LAMBDES，该工具集成了定理证明器SPASS，可以对模型进行自动推理。我们成功地将此方法和工具应用于模型的一致性检查。

This paper proposes a novel approach to the formal definition of the UML semantics. We distinguish the descriptive semantics from the functional semantics of modelling languages. The former defines which system is an instance of a model while the later defines the basic concepts underlying the models. In this paper, the descriptive semantics of class diagrams, interaction diagrams and state machine diagrams are defined by first order logic formulas. A translation tool is implemented and integrated with the theorem prover SPASS to enable automated reasoning about models. The formalisation and reasoning of models is then applied to model consistency checking.