Title: Developing an Automated Theorem Prover
Advisor: Tunga Güngör
Type: MS
Year: All
Status: Offered

---

In this project, a first-order and resolution-based automated theorem prover (ATP) will be developed. Literature survey on ATPs, resolution, resolution refinements, and first-order predicate calculus will be done. Also the structures and interior workings of some of the currently available ATP systems (e.g. Otter) will be studied. A new ATP will be designed and implemented. It is required that at least one contribution to the current research (e.g. a new refinement, a heuristic) be proposed. The system will be tested on standard theorem sets and its performance will be measured (in seconds or some other metric) and compared with other ATPs in detail.