The current trend is to apply refactoring at levels of abstraction above the code level. We present a new approach to formalize model refactorings. The approach is based on the semantics of a predefined set of fine-grain transformations (FGTs) that can be used to construct any refactoring, and relies on logic-based representations of the UML model. The proposed approach has many features: it gives the ability to detect and resolve conflicts; to remove redundancies; to find sequential dependencies between refactorings; and to increase parallelizing opportunities. In addition, it enables the end user to build their new refactorings. Based on the proposed formalism we also introduce a new technique to find automatically the order of a batch of refactorings.