Please use this identifier to cite or link to this item:
http://hdl.handle.net/20.500.11889/2090
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Plaisted, David A. | - |
dc.contributor.author | Yahya, Adnan | en_US |
dc.date.accessioned | 2016-10-08T06:45:12Z | - |
dc.date.available | 2016-10-08T06:45:12Z | - |
dc.date.issued | 2003-3 | - |
dc.identifier.uri | http://hdl.handle.net/20.500.11889/2090 | - |
dc.description.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 | - |
dc.language.iso | en | en_US |
dc.publisher | ResearchGate | en_US |
dc.subject.lcsh | Materials - Research - Computer network resources | - |
dc.subject.lcsh | Automatic theorem proving | - |
dc.subject.lcsh | Software reengineering | - |
dc.subject.lcsh | Object-oriented methods (Computer science) | - |
dc.title | A relevance restriction strategy for automated deduction | en_US |
dc.type | Article | en_US |
newfileds.department | Engineering and Technology | en_US |
newfileds.item-access-type | open_access | en_US |
item.fulltext | With Fulltext | - |
item.grantfulltext | open | - |
item.languageiso639-1 | other | - |
Appears in Collections: | Fulltext Publications |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
A_relevance_restriction_strategy_for_automated_ded.pdf | 370.41 kB | Adobe PDF | View/Open |
Page view(s)
126
Last Week
0
0
Last month
2
2
checked on Mar 25, 2024
Download(s)
48
checked on Mar 25, 2024
Google ScholarTM
Check
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.