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