Automated proving in planar geometry based on the complex number identity method and elimination

Zoltán Kovács, Xicheng Peng

We improve the complex number identity proving method to a fully automated procedure, based on elimination ideals. By using declarative equations or rewriting each real-relational…