In this paper we propose an approach to reason on UML schemas with OCL constraints. We provide a set of theorems to determine
that a schema does not have any infinite model and then provide a decidable method that, given a schema of this kind, efficiently
checks whether it satisfies a set of desirable properties such as schema satisfiability and class or association liveliness.
Keywords Conceptual modeling - Reasoning - Decidability