@TECHREPORT{BasinGanzinger-95-mpii2-006,                      
        AUTHOR             = {Basin, D. and Ganzinger, H.},
        ADDRESS            = SB,
        INSTITUTION        = MPI,
	TYPE               = {Technical Report},
        NUMBER             = {MPI-I-95-2-006},
        TITLE              = {Automated Complexity Analysis Based on Ordered Resolution},
        YEAR               = {1995},
        abstract = {
We define \emph{order locality} to be a property of clauses 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 clause.  We show that when a clause set is
order local, then the complexity of its ground entailment problem is
a function of 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 being saturated 
under ordered resolution.  This provides a means of using standard
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 entailment problems
relative to complexity classes which include Polynomial and
Exponential Time and co-NP. },

}