Name
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 unsafisfiable. 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 |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1016/S0004-3702(02)00368-5 | Artif. Intell. |
Keywords | Field | DocType |
clauses c,multiple set,relevance distance,relevance set r,distinguished set,support set,s. r,relevance restriction strategy,advanced relevance technique,automated deduction,different relevance metrics,relevance set,theorem proving,automated theorem proving,goal orientation,relevance | Discrete mathematics,Negation,Goal orientation,Automated theorem proving,If and only if,Unit propagation,Mathematics | Journal |
Volume | Issue | ISSN |
144 | 1-2 | 0004-3702 |
Citations | PageRank | References |
14 | 1.03 | 15 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| David A. Plaisted | 1 | 1680 | 255.36 |
| Adnan Yahya | 2 | 68 | 4.77 |