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.