Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barwise, B. & Etchemendy, J. (1999). Language, Proof and Logic. Seven Bridges Press. New York.
Chuaqui, R. & Suppes, P., (1990). An equational deductive system for the differential and integral calculus. In P. Martin-Lof & G. Mints, Eds., Lecture Notes in Computer Science, Proceedings of COLOG-88 International Conference on Computer Logic (Tallin, USSR). Berlin and Heidelberg: Springer Verlag, pp. 25–49.
Education Program for Gifted Youth (EPGY). Theorem Proving Environment Overview. http://epgy.stanford.edu/TPE.
Hearn, A. (1987). Reduce user’s manual, Version 3.3. (Report CP 78). The RAND Corporation. Santa Monica CA.
McCune, William. Otter 3.0 reference manual and guide. Technical Report ANL-94/6. Argonne National Laboratory. January 1994.
Ravaglia, R. (1990). User’s Guide for the Equational Derivation System. Education Program for Gifted Youth, Palo Alto.
Ravaglia R., Alper, T. M., Rozenfeld, M., & Suppes, P. (1998). Successful Applications of Symbolic Computation. In Human Interaction with Symbolic Computation,ed. N. Kajler. Springer-Verlag, New York, pp. 61–87.
Sieg, W., & Byrnes, J. (1996). Normal Natural Deduction Proofs (in classical logic).Tech-report CMU-PHIL-74. Department of Philosophy, Carnegie Mellon Univ., Pittsburgh,PA 15213.
Suppes, P. Ed.. (1981). University-level computer-assisted instruction at Stanford:1968–1980. Stanford, CA: Institute for Mathematical Studies of the Social Sciences, Stanford University.
Suppes, P. & Takahashi, S. (1989). An interactive calculus theorem-prover for continuity properties. Journal of Symbolic Computation, Volume 7, pp. 573–590.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McMath, D., Rozenfeld, M., Sommer, R. (2001). A Computer Environment for Writing Ordinary Mathematical Proofs. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_35
Download citation
DOI: https://doi.org/10.1007/3-540-45653-8_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42957-9
Online ISBN: 978-3-540-45653-7
eBook Packages: Springer Book Archive