Search

One of our goals is to formalize an equivalence class(FEC) of the fuzzy relational database(FRDB). FRDB, an extension of RDB using a soft computing technique, fuzzy theory. Using our relational formulas of relational calculus, we can denote its properties by simple and correct formulas. Also, we can prove its properties formally using relational calculus. There are many applications of FRDB such as managing hyperlinks of web pages, customer relationship management (CRM), etc. Our motivation is developing formal verification tools for a software system using FEC of FRDB. We also formalize database operations such as “projection”, “selection”, and “natural join”. We prove several elementary properties of natural join operations using our formalization.

We implemented operations appeared in the theory of automata using the Coq proof-assistant. A language which contains infinite elements is defined using ssreflect (a Small Scale Reflection Extension for the Coq system). We also implemented the modules for sticker systems. Paun and Rozenberg introduced a concrete method to transform an automaton to a sticker system in 1998. One of our aims is to present formal proofs of the correctness of their transformation. We modified some of their definitions to improve their insufficient results. We note that all of our formulation are written in Coq and we show some examples of machine-checkable proofs.