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):
Socher-Ambrosius, Rolfdblp

BibTeX cite key*:

socher92b

Title

Title*:

How to Avoid the Derivation of Redundant Clauses in Reasoning Systems

Journal

Journal Title*:

Journal of Automated Reasoning
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Kluwer
Publisher's URL:


Publisher's
Address:


ISSN:

0168-7433

Vol, No, pp, Date

Volume*:

9
Number:

1

Publishing Date:

1992

Pages*:

325-336
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

This paper addresses two problems concerning the issue of redundant information in resolution based reasoning systems. The first one deals with the question how the derivation of redundant clauses, such as duplicates or instances of already retained clauses, can be substantially reduced. The second one asks for a criterion to decide, which clauses need not be tested for reduncancy. In this paper we consider a particular kind of reduncancy, which we call {\em ancestor subsumption}, that is the subsumption of a resolvent by one of its ancestors. We give a complete syntactic characterization of clause sets producing ancestor subsumed clauses. This characterization partially answers the two questions. First, if a clause set is known to exclude ancestor subsumption, linear resolution turns out to be a preferable strategy in order to reduce the generation of subsumed clauses. Concerning the second question, this result allows a suitable restriction of the-usually very expensive-subsumption test. Finally,
we show that in particular cases those clauses that account for the occurrence of ancestor subsumption can be excluded from the resolution process. SAM's lemma will serve as an example for demonstrating various possibilities to remove reduncancy-generating clauses.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:


Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:


BibTeX Entry:
@ARTICLE{socher92b,
AUTHOR = {Socher-Ambrosius, Rolf},
 TITLE = {How to Avoid the Derivation of Redundant Clauses in Reasoning Systems},
 JOURNAL = {Journal of Automated Reasoning},
 PUBLISHER = {Kluwer},
 YEAR = {1992},
 NUMBER = {1},
 VOLUME = {9},
 PAGES = {325--336},
 ISBN = {0168-7433},
}

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)
Uwe Brahm		Created
01/14/1995 06:52:41 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Christine Kiesel
Uwe Brahm
Christine Kiesel/AG2/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE		Edit Dates
30.08.2001 10:14:04
16/03/97 00:44:23
03/02/95 16:58:01
21/01/95 20:56:05
17/01/95 20:08:48