In this paper, we propose the use of formal techniques on Software Engineering in two directions: 1)We present, within the general framework of lattice theory, the analysis of relational databases. To do that, we characterize the concept of f-family (Armstrong relations) by means of a new concept which we call non-deterministic ideal operator. This characterization allows us to formalize database redundancy in a more significant way than it was thought of in the literature. 2) We introduce the Substitution Logic SL _FD for functional dependencies that will allows us the design of automatic transformations of data models to remove redundancy.