The course covers fundamentals of propositional and predicate logic, and their uses in declarative programming to model and solve computational problems. Topics include propositional satisfiability, satisfiability testing techniques such as the DPLL algorithm, automated reasoning techniques for predicate logic such as resolution with unification and logic programming.
CS 315 and CS 375 or consent of instructor.
Students must be familiar with the syntax and basic properties of propositional and predicate logic, and mastery of programming in a high-level programming language.
Students will develop knowledge of propositional and predicate logic and their uses in declarative problem solving. Specifically, students will be able to:
Students are evaluated on their work (homeworks, exams). Students receive back their homework and exams. These papers are marked to indicate problems and they point out correct or better solutions. Problems that turn out to be especially difficult are discussed in class during lectures or during recitations.
NOTE: Since the course is open to both undergraduate and graduate students, different grading schemes are used for each group. Also, any grade normalization will be done against peer students, i.e. undergraduates will only be normalized with undergraduates, and graduates with graduates.
The instructor will assess the learning outcomes on the basis of students' work (homeworks, projects and exams) and students' self-assessment (the outcomes will be announced to students at the beginning of the semester; at the end of the semester the instructor will conduct a survey asking students to assess their mastery of the outcomes).
Logic for Applications, 2nd edition,
A. Nerode, R. Shore,
Springer Verlag, 1996.
From Logic to Logic Programming,
MIT Press, 1994.
From Logic Programming to Prolog,
K. R. Apt,
Advanced Programming Language Design,
Raphael A. Finkel,