Synthesis of Geometry Proof Problems

Authors

  • Chris Alvin Louisiana State University, Baton Rouge
  • Sumit Gulwani Microsoft Research
  • Rupak Majumdar Max Planck Institute for Software Systems
  • Supratik Mukhopadhyay Louisiana State University, Baton Rouge

DOI:

https://doi.org/10.1609/aaai.v28i1.8745

Keywords:

Problem Synthesis, Automated Reasoning, Computer-Aided Education, Interesting Problem, Complete Problem

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.

AAAI 2014 Proceedings Cover

Downloads

Published

2014-06-19

How to Cite

Alvin, C., Gulwani, S., Majumdar, R., & Mukhopadhyay, S. (2014). Synthesis of Geometry Proof Problems. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1). https://doi.org/10.1609/aaai.v28i1.8745

Issue

Vol. 28 No. 1 (2014): Twenty-Eighth AAAI Conference on Artificial Intelligence

Section

AAAI Technical Track: Applications