借助定理证明器简化有序仿射几何的公理化体系
Simplifying the axiomatization for the ordered affine geometry via a theorem prover
AI总结：
针对von Plato提出的含22条公理的有序仿射几何构造性公理化体系，研究发现公理I.7存在冗余，借助定理证明器证明可用更简单直观的新公理等价替换该复杂公理，实现公理化体系的简化。
摘要：
基于带向直线的序关系，并以构造性公理替代存在性公理，von Plato提出了有序仿射几何的构造性公理化方案。该有序仿射几何体系共有22条公理，其中公理I.7是关于三条直线（忽略其方向）的收敛性的内容。本文指出公理I.7存在大量冗余，并借助定理证明器证明，复杂的公理I.7可被一条更简单直观的新公理等价替换。
英文摘要：
Based on an ordering with directed lines and using constructions instead of existential axioms, von Plato proposed a constructive axiomatization of the ordered affine geometry. There are 22 axioms for the ordered affine geometry, of which the axiom I.7 is about the convergence of three lines (ignoring their directions). In this paper, we indicate that the axiom I.7 includes much redundancy, and demonstrate that the complicated axiom I.7 can be replaced equivalently with a simpler and more intuitive new axiom via a theorem prover.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
