A Computer Environment for Writing Ordinary Mathematical Proofs

The EPGY Theorem-Proving Environment is designed to help students write ordinary mathematical proofs. The system, used in a selection of computer-based proof-intensive mathematics courses, allows students to easily input mathematical expressions, apply proof strategies, verify logical inference, and apply mathematical rules. Each course has its own language, database of theorems, and mathematical inference rules. The main goal of the project is to create a system that imitates standard mathematical practice in the sense that it allows for natural modes of reasoning to generate proofs that look much like ordinary textbook proofs. Additionally, the system can be applied to an unlimited number of proof exercises.

• Type: Conference
• Year: 2001
• Where: LPAR
• Authors: David McMath, Marianna Rozenfeld, Richard Sommer
• Keywords: Automated Reasoning, LPAR 2001, Mathematical, Mathematical Inference Rules, Ordinary Mathematical Proofs