论文标题
地质 - 欧几里得几何形状的图形交互式定理谚语
GeoLogic -- Graphical interactive theorem prover for Euclidean geometry
论文作者
论文摘要
计算机中数学逻辑的域主要由自动定理掠夺（ATP）和交互式定理抛弃（ITP）主导。通过人为模拟方法，AI很难访问这两者：ATP经常使用人为不友好的逻辑基础，而ITP旨在正式化现有证明而不是解决问题。我们旨在创建一个简单的人类友好的逻辑系统，以解决数学问题。我们选择了欧几里得几何形状的案例研究，因为它可以很容易地可视化，具有简单的逻辑，但可能会提供许多各种难度水平的高中问题。为了使环境用户友好，我们放弃了ITP所需的严格逻辑，从而从图片中推断出拓扑事实。我们介绍了欧几里得几何形状的系统，以及类似于地理格拉的图形应用地质，该系统允许用户交互性地研究和证明有关几何设置的属性。
Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the human-imitation approach: ATPs often use human-unfriendly logical foundations while ITPs are meant for formalizing existing proofs rather than problem solving. We aim to create a simple human-friendly logical system for mathematical problem solving. We picked the case study of Euclidean geometry as it can be easily visualized, has simple logic, and yet potentially offers many high-school problems of various difficulty levels. To make the environment user friendly, we abandoned strict logic required by ITPs, allowing to infer topological facts from pictures. We present our system for Euclidean geometry, together with a graphical application GeoLogic, similar to GeoGebra, which allows users to interactively study and prove properties about the geometrical setup.
