@INPROCEEDINGS{BasinGanzinger96,
Author = "David Basin and Harald Ganzinger",
TITLE =		{Complexity Analysis Based on Ordered Resolution},
BOOKTITLE =		{Eleventh Annual IEEE Symposium on Logic in
                  Computer Science},
ADDRESS =		{New Brunswick, New Jersey, USA},
PUBLISHER =           {IEEE Computer Society Press},
YEAR =		{1996},
PAGES = {456 -- 465},
ABSTRACT = {We define order locality to be a property of clauses relative
to a term ordering.   This property is a kind of
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. }
 }