CS 251 Discrete Structures II

Credit Hours:

4

Course Coordinator:

Mark Jones and Suresh Singh

Course Description:

Continuation of CS 250. Logic: propositional calculus, first-order predicate calculus. Formal reasoning: natural deduction, resolution. Applications to program correctness and automatic reasoning. Introduction to algebraic structures in computing.

Prerequisites:

CS 250

Goals:

CS 251 is the second term of the two term sequence CS 250-251. The main goal of the sequence is that students obtain those skills in discrete mathematics and logic that are used in the study and practice of computer science.

Upon the successful completion of this class, students will be able to:

1. Apply the properties of propositional calculus to: determine whether a wff is a tautology, a contradiction, or a contingency by truth tables and by Quine's method; construct equivalence proofs; and transform truth functions and wffs into conjunctive or disjunctive normal form.
2. Describe the basic inference rules and use them to write formal proofs in propositional calculus.
3. Apply the properties of first-order predicate calculus to: determine whether a wff is valid, invalid, satisfiable, or unsatisfiable; construct equivalence proofs; and transform first-order wffs into prenex conjunctive or disjunctive normal form.
4. Describe the rules of inference for quantifiers and use them along with the basic inference rules to write formal proofs in first-order predicate calculus.
5. Write formal proofs in first-order predicate calculus with equality.
6. Transform first-order wffs into clausal form; and unify atoms from a set of clauses.
7. Describe the resolution inference rule; use it to write formal proofs in first-order logic; and describe how resolution is used to execute a logic program.
8. Transform simple English sentences into formal logic (propositional, first-order, or higher-order).
9. Apply appropriate algebraic properties to: simplify Boolean expressions; simplify regular expressions; write recursive definitions for simple functions in terms of operations for abstract data types; write expressions to represent relations constructed in terms of operations for relational databases; and work with congruences.

Major Topics:

• Propositional logic: propositional calculus, normal forms, formal reasoning.
• First-order logic: first-order predicate calculus, equivalence, quantifier inference rules.
• Applied Logic: equality, program correctness, higher-order logic.
• Automatic Reasoning: clausal forms, unification, resolution.
• Algebraic Structures: Boolean algebra, abstract data types, relational algebra, congruences.

Laboratory Exercises:

Several lab experiments are assigned (approximately one experiment per week) to reflect the classroom work. The experiments are similar in scope to homework exercises.

Oral and Written Communications:

Every student is required to submit 3 written reports (not including exams, tests, quizzes, or commented programs) of typically 10 pages in a lab notebook.

Theoretical Content:

The entire course is theoretical material (logic).

Problem Analysis:

The course is devoted to problem solving techniques of logic. The exercises and tests require problem analysis to find out which tools of formal logic are needed to solve a problem.

Solution Design:

The course is devoted to problem solving techniques of logic. The exercises and tests require students to solve problems by applying the tools of formal logic.