A Formal Approach to the Vertical Partitioning Problem in Distributed Database Design