ausblenden:
Schlagwörter:
-
Zusammenfassung:
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
the 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 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.
