zbMATH — the first resource for mathematics

A computer environment for writing ordinary mathematical proofs. (English) Zbl 1275.68128
Nieuwenhuis, Robert (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3–7, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42957-3/pbk). Lecture Notes in Computer Science 2250. Lecture Notes in Artificial Intelligence, 507-516 (2001).
Summary: 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.
For the entire collection see [Zbl 1046.03001].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
97U70 Technological tools, calculators (aspects of mathematics education)
Full Text: DOI