Abstract

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 [7], 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.

Advisor

Hartman, James

Second Advisor

Visa, Sofia

Department

Computer Science; Mathematics

Publication Date

2017

Degree Granted

Bachelor of Arts

Document Type

Senior Independent Study Thesis Exemplar

Download

Share

COinS
 

© Copyright 2017 Khoa Nguyen