This web site is no longer maintained and the content may be outdated.
Please visit www.cmpe.boun.edu.tr for up-to-date information.
 
CmpE RSS
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
Description

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: infocmpe.boun.edu.tr   webmaster: webmastercmpe.boun.edu.tr