Testing Satisfiability Of A Conjunction Of Inequalities

Conjunctions of inequality predicates, or inequalities for short, have been utilized to represent conjunctive queries and semantic integrity constraints in semantic query processing systems (Klug 1988, Ullman 1989, Shenoy and Ozsoyoglu 1989, Guo et al. 1996). In conjunctive query containment problem, one needs to check whether a conjunction or set of inequality predicates implies an inequality. This test is also applicable to checking redundant inequalities in an integrity constraint represented by a conjunction or to checking the satisfiability of a constraint. Ullman (1989) presents 8 axioms that calculate the transitive closure of a set of inequalities to check whether an inequality is implied by a conjunction or set of inequalities. The closure algorithm does not directly handle equality (or inequalities that imply equalities) predicates and constants in inequalities. In this paper, we extend the Ullman's closure algorithm by allowing constants and equalities (or rather inequalitie..