Modelling an Automatic Proof Generator for Functional Dependency Rules Using Colored Petri Net
This work addresses a specific need for database administrators in normalization and integrity enforcement, but it is incremental as it applies existing formal methods to a known problem.
The paper tackled the problem of automatically generating proofs for functional dependency rules in databases by modeling Armstrong's axioms using Colored Petri Nets, resulting in a method that can search for and extract proofs via model checking and recursive ML code.
Database administrators need to compute closure of functional dependencies (FDs) for normalization of database systems and enforcing integrity rules. Colored Petri net (CPN) is a powerful formal method for modelling and verification of various systems. In this paper, we modelled Armstrong's axioms for automatic proof generation of a new FD rule from initial FD rules using CPN. For this purpose, a CPN model of Armstrong's axioms presents and initial FDs considered in the model as initial color set. Then we search required FD in the state space of the model via model checking. If it exists in the state space, then a recursive ML code extracts the proof of this FD rule using further searches in the state space of the model.