Automated complexity analysis based on ordered resolution

We define order locality to be a property of clauses relative to a term ord ering. This property generalizes the subformula property for proofs where t he terms appearing in proofs can be bounded, under the given ordering, by t erms appearing in the goal clause. We show that when a clause set is order local, then the complexity of its ground entailment problem is a function o f its structure (e.g., full versus Horn clauses), and the ordering used. We prove that. in many cases, order locality is equivalent to a clause set be ing saturated under ordered resolution. This provides a means of using stan dard resolution theorem provers for testing order locality and transforming non-local clause sets into local ones. We have used the Saturate system to automatically establish complexity bounds for a number of nontrivial entai lment problems relative to complexity classes which include polynomial and exponential time and co-NP.