MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments

MPI-I-95-2-006

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: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1995-2-006

Hide details for BibTeXBibTeX
@TECHREPORT{BasinGanzinger95,
  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},
}