Theorem proving method for ERM-model formal system

«Entity - Relationship - Mapping» model (or ERM-model for short) is a semantic data modelpossessing a wide variety of expressive capabilities. It allows reflecting most features of the universeof discourse (UoD) at the stage of semantic modeling in human-oriented language. The seconddistinctive feature of this model is a presence of semantically significant mappings theory(SSMT) in its foundation. This theory with its rigorous mathematic formal system, grants the reliablerules of schema consistency checks, the rules of schema completion with additional integrityconstraints following from designer-defined constraints, and also the rules of effective and fulltransformation of ERM-schema into DBMS-oriented schema, particularly into relational schema.All these rules are based on the axioms and proved theorems of SSMT formal system. Duringthe process of new theorem proving there is constant improvement of formulas syntax and axiomaticbasis of formal system. Each proved theorem, on the one hand, expands the system, providinga basis for new theorems, and on the other hand, it helps to improve the rules of ERMmodelmentioned above.One of the theorems is used as an example for theorem proving method considered in this article.It becomes necessary to revise the formal system axiomatics during the process of theoremproving. This article deals with a new full axiom set.The method of the proving can be represented by the following steps.1. Put forward a hypothesis and formulate a theorem in terms of SSMT formal system.2. Define SSMT axioms and theorems necessary for the proof.3. Convert theorem and axioms formulae into the Skolem standard form.4. Formulate an initial theorem clause set.5. Prove by making use of resolution method, that a set of clauses is unsatisfiable.

Keywords

Authors

References