Consistency verification of deductive database schemes

A deductive database scheme consists of a set of base predicate schemes and a set of possibly non­ Horn clauses. A database can be considered as a particular instance of a given scheme. Clearly, a property that must be held by any scheme is logical consistency. We also propose other related properties (non-trivial consistency, strong consistency and P-consistency). These properties are requirements which are reasonable and meaningful in many practical cases. For verifying the various forms of consistency, we discuss a method whose centerpiece is a theorem prover which is an instance of a linear-resolution-based paradigm for first-order lheories, called SL* resolution