MPI-INF/SWS Research Reports 1991-2021

1. Author,Editor - 3. with BibTeX cite keys


Automated complexity analysis based on ordered resolution

Basin, David A. and Ganzinger, Harald

November 1995, 33 pages.

Status: available - back from printing

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.

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Basin, David A. and Ganzinger, Harald},
  TITLE = {Automated complexity analysis based on ordered resolution},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-95-2-006},
  MONTH = {November},
  YEAR = {1995},
  ISSN = {0946-011X},