Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Basin, David A.
Ganzinger, Harald		dblp
dblp
Not MPG Author(s):
Basin, David A.

BibTeX cite key*:

BasinGanzinger-01-jacm

Title

Title*:

Automated Complexity Analysis Based on Ordered Resolution


2001JACM.ps.gz (140.26 KB)

Journal

Journal Title*:

Journal of the ACM
Journal's URL:

http://www.acm.org/jacm/

Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

ACM
Publisher's URL:


Publisher's
Address:

New York, USA
ISSN:


Vol, No, pp, Date

Volume*:

48
Number:

1

Publishing Date:

2001

Pages*:

70-109
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

We define 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
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 nontrivial entailment problems
relative to complexity classes which include polynomial and
exponential time and co-NP.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:

\hgURL{~hg/pja.html#2001JACM}

Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@ARTICLE{BasinGanzinger-01-jacm,
AUTHOR = {Basin, David A. and Ganzinger, Harald},
 TITLE = {Automated Complexity Analysis Based on Ordered Resolution},
 JOURNAL = {Journal of the ACM},
 PUBLISHER = {ACM},
 YEAR = {2001},
 NUMBER = {1},
 VOLUME = {48},
 PAGES = {70--109},
 ADDRESS = {New York, USA},
}

Entry last modified by Christine Kiesel, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Christine Kiesel		Created
08/27/2001 08:24:22 PM
Revisions
11.
10.
9.
8.
7.		Editor(s)
Christine Kiesel
Christine Kiesel
Harald Ganzinger
Uwe Brahm
Uwe Brahm		Edit Dates
01.09.2003 17:14:52
23.07.2003 15:05:26
16.05.2003 10:42:51
03/28/2002 12:45:46 AM
18.01.2002 11:30:20
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

File Attachment Icon
2001JACM.ps.gz