@INPROCEEDINGS{BasinGanzinger-96-lics,                      
        AUTHOR             = {Basin, D. and Ganzinger, H.},
        BOOKTITLE          = {Proc.\ 11th IEEE Symposium on Logic in Computer Science},
        TITLE              = {Complexity Analysis Based on Ordered Resolution},
        YEAR               = {1996},
	PAGES		   = {456--465},
	PUBLISHER          = {IEEE Computer Society Press},
        abstract = {
  McAllester and Given have given procedures for recognizing certain
  sets of Horn clauses which generate polynomial time decidable
  entailment relations.  These clause sets have a property called {\em
    locality}, which corresponds to a kind of subformula property
  for Horn clause proofs.  We generalize locality and show that it is in
  many cases equivalent to a clause set being saturated up to redundancy
  under ordered resolution.  This provides a procedure, which we have
  implemented in the Saturate system, for testing locality and
  transforming non-local clause sets into local ones.  Our notion of
  locality is defined on full clauses and is relative to term-orderings;
  this allows us to use Saturate to automatically establish complexity
  bounds for entailment problems and algorithms relative to a variety of
  complexity classes, including PTime, co-NP, and Exponential Time.},

}