Synthesis of Geometry Proof Problems
Abstract
This paper presents a semi-automated methodology for generating geometric proof problems of the kind found in a high-school curriculum. We formalize the notion of a geometry proof problem and describe an algorithm for generating such problems over a user-provided figure. Our experimental results indicate that our problem generation algorithm can effectively generate proof problems in elementary geometry. On a corpus of 110 figures taken from popular geometry textbooks, our system generated an average of about 443 problems per figure in an average time of 4.7 seconds per figure.
Cite
Text
Alvin et al. "Synthesis of Geometry Proof Problems." AAAI Conference on Artificial Intelligence, 2014. doi:10.1609/AAAI.V28I1.8745Markdown
[Alvin et al. "Synthesis of Geometry Proof Problems." AAAI Conference on Artificial Intelligence, 2014.](https://mlanthology.org/aaai/2014/alvin2014aaai-synthesis/) doi:10.1609/AAAI.V28I1.8745BibTeX
@inproceedings{alvin2014aaai-synthesis,
title = {{Synthesis of Geometry Proof Problems}},
author = {Alvin, Chris and Gulwani, Sumit and Majumdar, Rupak and Mukhopadhyay, Supratik},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2014},
pages = {245-252},
doi = {10.1609/AAAI.V28I1.8745},
url = {https://mlanthology.org/aaai/2014/alvin2014aaai-synthesis/}
}