• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Conference on Energy Internet >Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic
【24h】

Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic

机译：基于强相关逻辑的前向推理在自动定理发现中测量定理的趣味性

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. The problem implicitly requires some metrics to be used for measuring interestingness of found theorems. A set of metrics for measuring interestingness of theorems in automated theorem finding by forward reasoning based on strong relevant logic have been proposed, and a case study to measure interestingness of the theorems of Tarski's geometry was performed. The result of the case study showed that the proposed metrics were hopeful for measuring interestingness of theorems in automated theorem finding. However, there is no research about the influence of different logical fragments of strong relevant logic on theorem finding. This paper presents a case study to measure interestingness of theorems obtained by using forward reasoning based on different logical fragments. The result shows that different logical fragments have different effects on the four factors of interestingness of theorems.
机译：自动定理的发现问题是Wos最初于1988年提出的33项自动推理的基础研究问题之一，至今仍是一个未解决的问题。该问题暗含要求使用一些度量标准来度量发现的定理的趣味性。提出了一套基于强相关逻辑的前向推理中自动定理发现中度量定理趣味性的度量标准，并进行了一个案例研究，以衡量Tarski几何定理的趣味性。案例研究的结果表明，所提出的度量标准对于测量定理在自动定理发现中的趣味性是有希望的。但是，还没有关于强相关逻辑的不同逻辑片段对定理发现的影响的研究。本文提出了一个案例研究，以衡量通过使用基于不同逻辑片段的正向推理获得的定理的趣味性。结果表明，不同的逻辑片段对定理趣味性的四个因素有不同的影响。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号