@Article{ basin.ea:automated:2001, abstract = {We define order locality to be a property of clauses relativeto a term ordering. This propertygeneralizes the subformula property for proofs wherethe terms appearing in proofs can be bounded,under the given ordering,by terms appearing in the goal clause. We show that when a clause set isorder local, then the complexity of its ground entailment problem isa function of its structure (e.g., full versus Horn clauses),and the ordering used. We prove that, in many cases, order localityis equivalent to a clause set being saturatedunder ordered resolution. This provides a means of using standardresolution theorem provers for testing order locality andtransforming non-local clause sets into local ones.We have used the Saturate system to automatically establish complexitybounds for a number of nontrivial entailment problemsrelative to complexity classes which include polynomial andexponential time and co-NP.}, author = {David Basin and Harald Ganzinger}, journal = {Journal of the Association of Computing Machinery}, month = {January}, number = 1, pages = {70--109}, language = {USenglish}, ps = {papers/2001/jacm01.ps.gz}, title = {Automated Complexity Analysis Based on Ordered Resolution}, volume = 48, year = 2001 }