Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Conference Paper

Complexity Analysis Based on Ordered Resolution


Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;


Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Basin, D. A., & Ganzinger, H. (1996). Complexity Analysis Based on Ordered Resolution. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96) (pp. 456-465). Los Alamitos, USA: IEEE.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-ABCB-3
We define \emph{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.