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

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.