Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Automated complexity analysis based on ordered resolution

Basin, David A. and Ganzinger, Harald

MPI-I-95-2-006. November 1995, 33 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-95-2-006.pdfMPI-I-95-2-006.pdf51108 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

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},