J.A.F.: An Efficient Proof Procedure for a Family of Lightweight Database Schemas

Abstract. This paper introduces procedures to test strict satisfiability and de-cide logical implication for a family of database schemas called extralite sche-mas with role hierarchies. Using the OWL jargon, extralite schemas support named classes, datatype and object properties, minCardinalities and maxCardi-nalities, InverseFunctionalProperties, class subset constraints, and class dis-jointness constraints. Extralite schemas with role hierarchies also support subset and disjointness constraints defined for datatype and object properties. Strict sa-tisfiability imposes the additional restriction that the constraints of a schema must not force classes or datatype or object properties to be always empty, and is therefore more adequate than the traditional notion of satisfiability in the con-text of database design. The decision procedures outlined in the paper are based on the satisfiability algorithm for Boolean formulas in conjunctive normal form with at most two literals per clause, and explore the structure of a set of con-straints, captured as a constraint graph. The paper includes a proof that the pro-cedures work in polynomial time and are consistent and complete for a subfa-mily of the schemas that impose a restriction on the role hierarchy