Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry
CoRR(2024)
摘要
The pursue of what are properties that can be identified to permit an
automated reasoning program to generate and find new and interesting theorems
is an interesting research goal (pun intended). The automatic discovery of new
theorems is a goal in itself, and it has been addressed in specific areas, with
different methods. The separation of the "weeds", uninteresting, trivial facts,
from the "wheat", new and interesting facts, is much harder, but is also being
addressed by different authors using different approaches. In this paper we
will focus on geometry. We present and discuss different approaches for the
automatic discovery of geometric theorems (and properties), and different
metrics to find the interesting theorems among all those that were generated.
After this description we will introduce the first result of this article: an
undecidability result proving that having an algorithmic procedure that decides
for every possible Turing Machine that produces theorems, whether it is able to
produce also interesting theorems, is an undecidable problem. Consequently, we
will argue that judging whether a theorem prover is able to produce interesting
theorems remains a non deterministic task, at best a task to be addressed by
program based in an algorithm guided by heuristics criteria. Therefore, as a
human, to satisfy this task two things are necessary: an expert survey that
sheds light on what a theorem prover/finder of interesting geometric theorems
is, and - to enable this analysis - other surveys that clarify metrics and
approaches related to the interestingness of geometric theorems. In the
conclusion of this article we will introduce the structure of two of these
surveys - the second result of this article - and we will discuss some future
work.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要