CS 555 - Declarative Programming

 

Credits: 3

 

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

 

Prereqs: CS 315 and CS 375 or consent of instructor.

 

Needed Skills

 

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.

 

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.

 

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

 

CAC Categories

 

Topic

Core

Advanced

Math Fundamentals

8

10

Data Structures

0

0

Algorithms & Software Design

10

10

Computer Organization and Architecture

0

0

Concepts of Programming Languages

6

0

Social and ethical issues

1

0

Total

25

20

 

Math Fundamentals (18):

Core (8): propositional logic, tautologies, satisfiability, provability

Advanced (10): predicate logic, prenex form, skolemization, normal form, universal theories, models and Herbrand models, soundness, completeness

 

Algorithms and Software Design (20):

Core (10): truth-table technique, propositional tableaux, DPLL procedure, modeling instances of search problems as propositional theories

Advanced (10): unification, resolution, resolution-refutation, grounding

 

Concepts of Programming Languages (6): Core (6): principles of declarative programming, propositional and predicate logics as programming languages, logic programming

 

Social and Ethical Issues (1): Discussion of professional and academic integrity

 

Oral Communication (presentations)

 

none

 

Written Communication

 

8-10 homeworks and projects, 2 pages/assignment

 

Coverage

 

Theoretical Content: 50%

Study propositional logic, its syntax and semantics; tautologies, and contradictions; satisfiability, propositional resolution and resolution refutation; soundness and completeness; predicate logic, its syntax and semantics; prenex form, skolemization, normal form, universal theories, models and Herbrand models, unification, resolution, resolution-refutation, grounding, soundness, completeness

 

Problem Analysis: 25%

Formulate and study properties of propositional and predicate logic theories, relate search problems to logic theories, view logic as a high-level specification language

 

Solution Design: 25%

Construct proofs of properties of logic theories; construct resolution and resolution-refutation proofs of entailment, construct encodings of search problems as logic theories; solve search problems by means of automated reasoning techniques (satisfiability checkers, resolution provers)

 

Student Evaluation and Feedback

 

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.

 

Grading

 

For the graduate students with score S on the scale from 0 to 100:

 

S ≥ 93

A

93 > S ≥ 82

B

82 > S ≥ 71

C

60 > S

E (fail)

 

For the undergraduate students with score S on the scale from 0 to 100:

 

S ≥ 90

A

90 > S ≥ 80

B

80 > S ≥ 70

C

70 > S ≥ 60

D

60 > S

E (fail)

 

Course Evaluation Questions

 

The course has taught me how to:

37. Test satisfiability of propositional theories.

38. Construct Herbrand interpretations and models of first-order theories.

39. Convert first-order theories into their clausal normal forms.

40. Construct resolution and resolution-refutation proofs.

41. Encode instances of search problems as propositional theories.

42. Encode search problems as theories in predicate logic and its variants.

 

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.