CS 555 - Declarative Programming

Bulletin Description

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.

Expected Preparation

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.

Student Learning Outcomes

Students will develop knowledge of propositional and predicate logic and their uses in declarative problem solving. Specifically, students will be able to:

  1. Use techniques of propositional logic to test satisfiability of propositional theories.
  2. Construct Herbrand interpretations and models of first-order theories.
  3. Convert first-order theories into their clausal normal forms.
  4. Construct resolution and resolution-refutation proofs.
  5. Encode instances of search problems as propositional theories.
  6.  Encode search problems as theories in predicate logic and its variants.


Direct Measures:

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.

Indirect Measures:

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

Syllabus Information

Possible Textbooks:

Logic for Applications, 2nd edition,
A. Nerode, R. Shore,
Springer Verlag, 1996.

From Logic to Logic Programming,
K. Doets,
MIT Press, 1994.

From Logic Programming to Prolog,
K. R. Apt,
Prentice-Hall, 1997.

Advanced Programming Language Design,
Raphael A. Finkel,
Addison-Wesley, 1996.