English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Automated Complexity Analysis Based on Ordered Resolution

Basin, D. A., & Ganzinger, H. (2001). Automated Complexity Analysis Based on Ordered Resolution. Journal of the ACM, 48(1), 70-109.

Item is

Files

show Files
hide Files
:
2001JACM.ps.gz (Any fulltext), 141KB
 
File Permalink:
-
Name:
2001JACM.ps.gz
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/gzip
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Basin, David A.1, Author           
Ganzinger, Harald1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-122001
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: eDoc: 519834
Other: Local-ID: C1256104005ECAFC-28522DC6EE4FC3B0C1256AB500651BA7-BasinGanzinger-01-jacm
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Journal of the ACM
Source Genre: Journal
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 48 (1) Sequence Number: - Start / End Page: 70 - 109 Identifier: -