On the Integrity of Typed First Order Data Bases

A typed first order data base is a set of first order formulae, each quantified variable of which is constrained to range over some type. Formally, a type is simply a distinguished monadic relation, or some Boolean combination of these. Assume that with each data base relation other than the types is associated an integrity constraint which specifies which types of individuals are permitted to fill the argument positions of that relation. The problem addressed in this paper is the detection of violations of these integrity constraints in the case of data base updates with universally quantified formulae. The basic approach is to first transform any such formula to its so-called reduced typed normal form, which is a suitably determined set of formulae whose conjunction turns out to be equivalent to the original formula. There are then simple criteria which, when applied to this normal form, determine whether that formula violates any of the argument typing integrity constraints.