Authors ' Addresses

We define order locality to be a property of dauses relative to a term ordering. This property is a generalization of the subformula property for proofs where terms arising in proofs are bounded, under the given ordering, by terms appearing in the goal dause. We show that when a dause set is order local, then the complexity of its ground entailment problem is a function of its structure (e.g., full versus Horn dauses), and the ordering used. We prove that, in many cases, order locality is equivalent to a dause set being saturated under ordered resolution. This provides a means of using standard resolution theorem provers for testing order locality and transforming non-Iocal dause sets into local ones. We have used the Saturate system to automatically establish complexity bounds for a number of nontrivial entailment problems relative to complexity dass e