Modelling an Automatic Proof Generator for Functional Dependency Rules Using Colored Petri Net

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, the authors 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, they 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.