Name
Abstract | ||
|---|---|---|
We define order locality to be a property of clauses relative to a term ordering. This property generalizes 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 nontrival entailment problems relative to complexity classes which include polynomial and exponential time and co-NP. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1145/363647.363681 | Journal of the ACM (JACM) |
Keywords | DocType | Volume |
first-order theories,goal clause,ground entailment problem,ordered resolution,clause set,automated theorem proving,complexity class,Automated complexity analysis,nontrival entailment problem,Horn clause,complexity bound,complexity analysis,order locality,subformula property,non-local clause set | Journal | 48 |
Issue | ISSN | Citations |
1 | 0004-5411 | 36 |
PageRank | References | Authors |
1.53 | 10 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David A. Basin | 1 | 4930 | 281.93 |
| Harald Ganzinger | 2 | 1513 | 155.21 |