Please use this identifier to cite or link to this item:

`http://hdl.handle.net/20.500.11889/2090`

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 |

URI: | http://hdl.handle.net/20.500.11889/2090 |

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 |

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