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

Home / Courses / CmpE 542
  CmpE 542    

Automated Theorem Proving

Description: Review of prepositional and first-order logic. Herbrand’s theorem. The resolution principle. Semantic resolution and lock resolution. Linear resolution. The equality relation. Some proof procedures based on Herbrand’s theorem. Program analysis. Deductive question answering, problem solving and program synthesis. Implementation of a theorem prover.

Course Offerings:

Fall 2013Tunga Güngör
Fall 2012Tunga Güngör
Fall 2010Tunga Güngör
Fall 2009Tunga Güngör
Fall 2008Tunga Güngör
Fall 2007Tunga Güngör
Fall 2006Tunga Güngör
Fall 2005Tunga Güngör
Fall 2004Tunga Güngör
Fall 2003Tunga Güngör
Spring 2003Tunga Güngör
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: