CmpE 542 Automated Theorem Proving 

Catalog 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.


(3+0+0) 3 ECTS 10


Consent of the instructor
Link Year Semester Course Page Instructor Course Schedule Lab Schedule PS Schedule
view 2013 Fall Course Page Tunga Güngör
view 2012 Fall Course Page Tunga Güngör
view 2010 Fall Tunga Güngör

Contact us

Department of Computer Engineering, Boğaziçi University,
34342 Bebek, Istanbul, Turkey

  • Phone: +90 212 359 45 23/24
  • Fax: +90 212 2872461

Connect with us

We're on Social Networks. Follow us & get in touch.