Twee风格目标导向性的若干实验
Some Experiments with Twee-Style Goal-Directedness
首次发表
浏览论文内容
中文总结 AI 辅助
针对饱和式定理证明中待处理子句的选择问题，将Twee的共享项优先思路推广到完整一阶情形，提出基于共享项的替代实现并取得良好结果。
中文摘要 AI 辅助
在饱和式定理证明中，选择下一个待处理子句是核心问题。Twee通过添加等式定义转换问题，成功应用了优先选择与猜想共享项的思路。本文将该思路推广到完整一阶情形，提供了一种基于共享项的替代实现，展现出极具前景的结果。
英文摘要
In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational definitions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms. Both approaches have complementary applications and show very promising results.
发表机构
- DHBW Stuttgart（施图加特双元州立大学）
机构由 AI 辅助整理，请以论文原文为准。
