Please use this identifier to cite or link to this item:
Title: A relevance restriction strategy for automated deduction
Authors: Plaisted, David A.
Yahya, Adnan
Issue Date: Mar-2003
Publisher: ResearchGate
Abstract: Identifying relevant clauses before attempting a proof may lead to more efficient automated theorem proving. Relevance is here defined relative to a given set of clauses S and one or more distinguished sets of support T . The role of a set of support T can be played by the negation of the theorem to be proved or the query to be answered in S which gives the refutation search goal orientation. The concept of relevance distance between two clauses C and D of S is defined using various metrics based on the properties of paths connecting C to D. This concept is extended to define relevance distance between a clause and a set (or multiple sets) of support. Informally, the relevance distance reflects how closely two clauses are related. The relevance distance to one or more support sets is used to compute a relevance set R, a subset of S that is unsatisfiable if and only if S is unsatisfiable. R is computed as the set of clauses of S at distance less than n from one or more support sets; if n is sufficiently large then R is unsatisfiable if S is. If R is much smaller than S, a refutation from R may be obtainable in much less time than a refutation from S. R must be efficiently computable to achieve an overall efficiency improvement. Different relevance metrics are defined, characterized and related. The tradeoffs between the amount of effort invested in computing a relevance set and the resulting gains in finding a refutation are addressed. Relevance sets may be utilized with arbitrary complete theorem proving strategies in a completeness-preserving manner. The potential of the advanced relevance techniques for various applications of theorem proving is discussed
Appears in Collections:Fulltext Publications

Files in This Item:
File Description SizeFormat
A_relevance_restriction_strategy_for_automated_ded.pdf370.41 kBAdobe PDFView/Open
Show full item record

Page view(s)

Last Week
Last month
checked on Jan 2, 2022


checked on Jan 2, 2022

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.