Simplifying von Plato's axiomatization of constructive apartness geometry (Q1964142)

\textit{J. von Plato} [Ann. Pure Appl. Logic 76, No. 2, 169-200 (1995; Zbl 0836.03034)], proposed quantifier-free intuitionistic axiom systems for affine and projective geometry, each being an extension of a rather weak common base, consisting of 14 axioms, called apartness geometry. By replacing three pairs of axioms with three axioms, as well as simplifying one of von Plato's axioms for apartness geometry, the authors obtain a new, equivalent axiom system with 11 axioms. The proofs of the equivalence of the new axiom system with von Plato's, as well as the search for the new axioms was assisted by an automated theorem prover, called Automated Natural Deduction Prover (ANDP). An appendix includes the print-outs of ANDP's proofs.