Automated Generation of Illustrations for Synthetic Geometry Proofs

TL;DR

This paper presents a modular system that automatically generates clear, animated illustrations for synthetic geometry proofs using the Larus prover and GCLC language, enhancing understanding and visualization.

Contribution

It introduces a novel, flexible approach combining automated proof generation with illustration creation, including animation support, for synthetic geometry.

Findings

Automated proof and illustration generation system developed

Supports animated illustrations for better visualization

Enhances comprehension of synthetic geometry proofs

Abstract

We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated using the Larus automated prover for coherent logic, and corresponding illustrations are generated in the GCLC language. Animated illustrations are also supported.