• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of symbolic computation >Towards a unified model of search in theorem-proving: subgoal-reduction strategies
【24h】

Towards a unified model of search in theorem-proving: subgoal-reduction strategies

机译：在定理证明中寻求统一的搜索模型：子目标减少策略

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

摘要

This paper advances the design of a unified model for the representation of search in first-order clausal theorem-proving, by extending to tableau-based subgoal-reduction strategies (e.g., model-elimination tableaux), the marked search-graph model, already introduced for ordering-based strategies, those that use (ordered) resolution, paramodulation/superposition, simplification, and subsumption. The resulting analytic marked search-graphs subsume AND-OR graphs, and allow us to represent those dynamic components, such as backtracking and instantiation of rigid variables, that have long been an obstacle to modelling subgoal-reduction strategies properly. The second part of the paper develops for analytic marked search-graphs the bounded search spaces approach to the analysis of infinite search spaces. We analyze how tableau inferences and backtracking affect the bounded search spaces during a derivation. Then, we apply this analysis to measure the effects of regularity and lemmatization byfolding-up on search complexity, by comparing the bounded search spaces of strategies with and without these features. We conclude with a discussion comparing the marked search-graphs for tableaux, linear resolution, and ordering-based strategies, showing how this search model applies across these classes of strategies.
机译：本文通过将基于标记的搜索图模型扩展到基于Tableau的子目标减少策略（例如，模型消除Tableaux），从而改进了用于在一阶子句定理证明中表示搜索的统一模型的设计。引入了基于排序的策略，即使用（排序的）分辨率，副调制/叠加，简化和包含的策略。生成的解析标记搜索图包含AND-OR图，并允许我们表示那些动态成分，例如回溯和刚性变量的实例化，这些因素长期以来一直是正确地建模子目标减少策略的障碍。本文的第二部分针对解析标记搜索图展开了有界搜索空间方法，以分析无限搜索空间。我们分析表格推论和回溯如何在推导过程中影响有限的搜索空间。然后，我们通过比较具有和不具有这些功能的策略的有限搜索空间，通过折叠对搜索复杂度的方法，应用此分析来衡量规则性和词条化的影响。最后，我们进行了讨论，比较了标记的搜索图，表格搜索，线性分辨率和基于排序的策略，显示了此搜索模型如何应用于这些策略类别。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号