BriefGPT.xyz
Jan, 2024
迈向自动可读的直尺和圆规构造证明
Towards Automated Readable Proofs of Ruler and Compass Constructions
HTML
PDF
Vesna Marinković, Tijana Šukilović, Filip Marić
TL;DR
本论文展示了我们的三角形构造求解器 ArgoTriCS 如何与一阶逻辑和连续逻辑的自动定理证明器合作，从而生成既可读性强的合成正确性证明，又具有形式化特性的构造解决方案。这些证明依赖于许多高级引理，我们的目标是从几何的基本公理中形式化证明它们全部。
Abstract
Although there are several systems that successfully generate
construction steps
for
ruler and compass construction problems
, none of them provides readable
→