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

TL;DR

This paper presents a formal method using Colored Petri Nets to automatically generate proofs of functional dependency rules in database normalization, enhancing verification and automation in database design.

Contribution

It models Armstrong's axioms within a Colored Petri Net framework to automate proof generation of functional dependencies.

Findings

Successfully models Armstrong's axioms with CPN

Automates proof extraction of FD rules

Enables verification via model checking

Abstract

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.