Abstract
We propose a logical procedure for the horizontal fragmentation problem based on predicate abstraction over the entire domain of database relations. The set of minterm predicates is constructed using rewriting rules similar to the well-known semantic tableau algorithm. The procedure start from an initial set of simple predicates, build the set of minterm predicates until rules are no longer required. To ensure this proposition, we give a formal proof of its correctness namely, it’s soundness, completeness and termination with Isabelle proof assistant. The main contribution of this work are: refining the minterm approach by adding a semantic layer to predicates, minimizing the set of minterm predicates by automatically eliminating contradictory ones, detecting and handling subsumptions between them. This leads to the best construction time of the final partitioning schema. Finally, a source code of the procedure is generated automatically by the Isabelle proof assistant.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ceri, S., Negri, M., Pelagatti, G.: Horizontal data partitioning in database design. In: Proceedings of the 1982 ACM SIGMOD International Conference on Management of Data, SIGMOD 1982, pp. 128–136. ACM, New York (1982)
Bellatreche, L., Karlapalem, K., Simonet, A.: Algorithms and support for horizontal class partitioning in object-oriented databases. Distrib. Parallel Databases 8(2), 155–179 (2000)
Ceri, S., Pelagatti, G.: Distributed Databases: Principles and Systems. McGraw-Hill Computer Science Series. McGraw-Hill, New York (1984)
Ozsu, M.T.: Principles of Distributed Database Systems, 3rd edn. Prentice Hall Press, Upper Saddle River (2007)
Dimovski, A., Velinov, G., Sahpaski, D.: Horizontal partitioning by predicate abstraction and its application to data warehouse design. In: Catania, B., Ivanović, M., Thalheim, B. (eds.) ADBIS 2010. LNCS, vol. 6295, pp. 164–175. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15576-5_14
Nipkow, T., Wenze, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Salmi, C., Chaabani, M., Mezghiche, M. (2018). A Formalized Procedure for Database Horizontal Fragmentation in Isabelle/HOL Proof Assistant. In: Abdelwahed, E., Bellatreche, L., Golfarelli, M., Méry, D., Ordonez, C. (eds) Model and Data Engineering. MEDI 2018. Lecture Notes in Computer Science(), vol 11163. Springer, Cham. https://doi.org/10.1007/978-3-030-00856-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-030-00856-7_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00855-0
Online ISBN: 978-3-030-00856-7
eBook Packages: Computer ScienceComputer Science (R0)