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.

Credits: 

(3+0+0) 3 ECTS 10

Prerequisites: 

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

Bize Ulaşın

Bilgisayar Mühendisliği Bölümü, Boğaziçi Üniversitesi,
34342 Bebek, İstanbul, Türkiye

  • Telefon: +90 212 359 45 23/24
  • Faks: +90 212 2872461
 

Bizi takip edin

Sosyal Medya hesaplarımızı izleyerek bölümdeki gelişmeleri takip edebilirsiniz