This project explores the theories of automated theorem proving and lambda calculus, and seeks to improve upon a current implementation of an automated theorem prover that produces human-like output. This software component is based on a published article titled “A Fully Automatic Theorem Prover with Human-Style Output” by M. Ganesalingam and W.T. Gowers , which outlines a program called robotone containing a first-order logic system (with a few modifications) able to automatically write simple direct proofs. It is designed to mimic different strategies that a human mathematician would use when facing a problem, and to write human-style proofs. The current prototype can solve and write eighteen proofs, seven of which are developed from this project with the addition of a mathematics library customized for the course MATH-332 Real-Analysis I at The College of Wooster. Future work includes further investigation on how human mathematicians construct their proofs, and a possible implementation of a more dynamic tactic mechanism to emulate humans’ thinking process better.
Computer Science; Mathematics
Nguyen, Khoa, "Pretending To Be Human: An Automated Theorem Prover To Write Mathematical Proofs" (2017). Senior Independent Study Theses. Paper 8308.
Bachelor of Arts
Senior Independent Study Thesis Exemplar
© Copyright 2017 Khoa Nguyen