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 8

Prerequisites: 

Consent of the instructor

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