hide
Free keywords:
-
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.
