15-819K Logic Programming

Fall 2006

Frank Pfenning

TuTh 10:30-11:50

WeH 4623

12 units

Logic programming is a paradigm where computation arises from proof search in a logic according to a fixed, predictable strategy. It thereby unifies logical specification and implementation in a way that is quite different from functional or imperative programming. This course provides a thorough, modern introduction to logic programming. It consists of a traditional lecture component and a project component. The lecture component introduces the basic concepts and techniques of logic programming followed by successive refinement towards more efficient implementations or extensions to richer logical concepts. We plan to cover a variety of logics and operational interpretations. The project component will be one or several projects related to logic programming.

Prerequisites: For undergraduates, 15-317 Constructive Logic or 15-312 Foundations of Programming Languages. No prerequisites for graduate students.

What's New?

(1/2) Bibliography of all cited references (source in BibTeX format)
(1/2) Complete set of lecture notes, a concatenation of all individual notes plus a cover page
(1/2) Notes for Lecture 19: Verify Progress
(12/31) Notes for Lecture 27: Constraint Logic Programming
(12/26) Notes for Lecture 26: Datalog

Class Material

Schedule	Lecture schedule, readings, code
Assignments	Details of assignments, due dates, policies
Projects	Project information
Handouts	Collected handouts
Software	Supporting software
Resources	Other course resources

Course Information

Lectures	TuTh 10:30-11:50, WeH 4623
Office Hours	Wed 11:00-12:00, WeH 8117
Notes	There is no textbook, but notes on Logic Programming and papers will be handed out
Credit	12 units
Grading	30% Homework, 15% Midterm, 55% Project
Homework	Weekly homework is assigned each Thursday and due the following Thursday.
Midterm	Date Thu Oct 19, in class. Closed book.
Project	Project topic or topics will be selected after the midterm.
Topics	Horn logic, intuitionistic logic, linear logic, unification, constraints, backward chaining, backtracking, forward chaining, saturation, proof terms, higher-order patterns, concurrency, resource management, logical compilation. Time permitting: deontic, epistemic, or other modal logics, reasoning about logic programs.
Mailing List	lp-course@cs [.cmu.edu]
Home	http://www.cs.cmu.edu/~fp/courses/lp/

fp@cs
Frank Pfenning