• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Artificial intelligence >A relevance restriction strategy for automated deduction
【24h】

A relevance restriction strategy for automated deduction

机译：自动扣除的关联性限制策略

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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 5 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.
机译：在尝试证明之前识别相关条款可能会导致更有效的自动定理证明。在此，相对于给定的一组子句S和一个或多个不同的支持集T定义相关性。可以通过否定要证明的定理或要回答的查询来发挥支持集T的作用。给出反驳搜索目标的方向。基于连接C到D的路径的属性，使用各种度量来定义S的两个子句C和D之间的相关距离的概念。此概念得到扩展，以定义一个子句与一组（或多组）支持之间的相关距离。非正式地，关联距离反映了两个子句之间的关联程度。与一个或多个支持集的关联距离用于计算关联集R，S是当且仅当5个不满足时，S的子集才不满足。 R被计算为与一个或多个支撑集之间的距离小于n的S子句集；如果n足够大，则S不满足R的要求。如果R远小于S，则与R的反驳可能比R的反驳少得多。R必须能够有效地计算以实现整体效率的提高。定义，表征和关联了不同的相关性度量。解决了在计算关联集时投入的精力与找到反驳所获得的收益之间的折衷。相关集可以以完整性保全的方式与任意完整定理证明策略一起使用。讨论了高级相关技术在定理证明的各种应用中的潜力。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号