Towards automated proving in solid geometry

Abstract

We present an approach for automated theorem proving in 3D solid geometry utilizing multiple algebraic prover engines. Our solution integrates dynamic geometry systems capable of generating solid geometry constructions. We have employed two different methods to transform geometric statements into algebraic representations, while implementing and evaluating these approaches with various theorem provers. Furthermore, we have explored non-degeneracy conditions (NDG) in the context of 3D solid geometry and provided insights into their role in ensuring the validity of geometric relations.