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.