摘要：简化公理系统,例如用短的公理代替长的公理,用少的公理替换多的公理,是定理证明领域中的一个方向,例如文章[6]中报告用一个公理代替群论的五个公里.请参看文章[5-10].本文将报告如何用定理证明器ANDP简化von Plato的构造性正交几何.ANDP是基于自然演绎的定理证明器,自然演绎是由Gentzen系统改进而来的,在文献[3]中已报道如何简化von Plato的一个公理.von Plato的构造性正交几何由22个公理组成,其中14个公理用来描述apartness几何.通过添加公里Al及A2到Apartness几何,得到Affine几何(仿射几何);再添加公理O1,O2,O3及O4到仿射几何得到正交几何.本文报告如何通过使用定理证明器来简化公理O1,O2及O4.关于如何简化apartness几何公理系统,请参看文献[3].
