This web site is no longer maintained and the content may be outdated.
Please visit for up-to-date information.
No upcoming events...

Home / Graduate / Offered-Ongoing MS-PhD Theses
  Thesis Topic Details    

Title: Developing an Automated Theorem Prover
Advisor: Tunga Güngör
Type: PhD
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.
Boğaziçi University Department of Computer Engineering
Address: 34342 Bebek, Istanbul, TURKEY
Phone: +90 212 359 4523-24 Fax: +90 212 287 2461
general information:   webmaster: