利用着色 Petri 网建模函数依赖规则的自动证明生成器
数据库
2012-10-12 v1 形式语言与自动机理论
软件工程
摘要
数据库管理员需要计算函数依赖（FDs）的闭包，以进行数据库系统的规范化并实施完整性规则。着色 Petri 网（CPN）是一种用于各种系统建模和验证的强大形式化方法。在本文中，我们利用 CPN 对 Armstrong 公理进行了建模，以实现从初始 FD 规则自动生成新 FD 规则的证明。为此，本文提出了 Armstrong 公理的 CPN 模型，并将初始 FDs 视为模型中的初始颜色集。随后，我们通过模型检查在模型的状态空间中搜索所需的 FD。如果该 FD 存在于状态空间中，则递归的 ML 代码会利用对模型状态空间的进一步搜索来提取该 FD 规则的证明。
引用
@article{arxiv.1210.3307,
title = {Modelling an Automatic Proof Generator for Functional Dependency Rules Using Colored Petri Net},
author = {Saeid Pashazadeh and Maryam Pashazadeh},
journal= {arXiv preprint arXiv:1210.3307},
year = {2012}
}
备注
17 pages, 4 figures