CISC 310: Logic and Programming

Catalog Description:
Propositional and predicate logic syntax, semantics; proof methods based on unification and resolution; applications involving translation, reasoning, and logic programming.

Current Texts:
Logic for Computer Scientists
U. Schöning
Birkhäuser Boston, 1989

Programming in Prolog, 4th Edition
W. F. Clocksin and C. S. Mellish
Springer-Verlag, Berlin, 1994.

Goals:
In computer science we see the automation of reasoning, the use of logic for knowledge representation in artificial intelligence and in data base theory and practice; the creation and use of logic programming languages such as Prolog; the use of logic for proving programs correct; and extensions of logic for formal specification, semantics, and design of programming languages.

In this course we will study in detail sound and complete logical systems with important expressive power. We will study a proof technique called resolution and disproof techniques based on semantic structures. Resolution is particularly suitable for automation! We will show how special cases of the logical systems and refinements of resolution naturally leads to the programming language Prolog in which the student will do some projects. Additionally, there will be some non-programming homeworks in which the student will have the opportunity to solve some problems and do some mathematical proofs.

Content:

• Propositional logic syntax and truth table semantics; conjunctive and disjunctive normal forms; Horn formulas; and propositional logic resolution.
• Quantifier and predicate logic syntax and model theoretic semantics; translation from English to predicate logic; prenex, Skolem and clausal forms; unification and predicate logic resolution; and logic programming.

Prerequisites:
CISC 220 (Data Structures), CISC 280 (Programming Paradigms), Math 315 (Discrete Math II).