CSE 360: LOGIC and COMPUTATION
Spring 1995 Semester
Venue: Tue, Thu 12:00-1:30, Moore 224
lectures /
homeworks /
modules
*** The following course description is a small part of the final
class. Only those parts particularly related to lambda Prolog are
included here. ***
Course Description: This course should prove useful to anyone
interested in computational uses of logic, especially those interested
in Cognitive Science and Programming Languages. Logic programming
will be taught and used in class to solve problems in cogitive
science, AI, and programming languages.
- Syntax, proof theory, model theory, and operational semantics of
various logics (classical, intuitionistic,
linear).
- Presentation of the logic programming paradigm using the
lambda Prolog language. This programming language incorporates
large amounts of logic and will be used to illustrate and apply
logical principles.
- Topics: typed lambda-calculus; propositions-as-types; natural
deduction; sequent calculus; cut-elimination; implementations of
natural deduction and sequent calculi; tactics and tacticals; proof
and program transformations; explanation based generalization;
parsing-as-deduction; meta-level and object-level distinctions; and
classical, intuitionistic, linear, and modal logics.
Prerequisites: CSE 120 and some sophistication with proofs by
induction (CSE 260 or Phil 5/6)
Textbook: "lambda Prolog: An Introduction to the Language and its Logic"
(current draft) by Dale Miller.
Additional course notes will also be used.
Grading: A combination of homework assignments, in-class
exams, and (possibly) a final will be used to determine grades.
It is expected that all homework is the work of individuals working
independently.
Course Outline
- Simple types; Curry-Howard Isomorphism; propositional
intuitionistic logic.
- Syntax and operational semantics of Prolog and lambda Prolog;
kinds, types, modules, abstract datatypes.
- Inference rules; natural deduction; Horn clauses as natural deduction.
- Computation as proof-search versus proof-reduction; comparison
of logic programming and functional programming.
- Unification, depth-first search, backtracking.
- Deductive databases; hypothetical reasoning; module importing.
- lambda-calculus, lambda-conversion, unification of
lambda-terms; meta-level and object-level distinctions.
- Higher-order programming in logic programming; tactic-style
theorem provers.
- Explanation based generalization; theorem proving strategies;
parsing-as-deduction; program transformation; specifications of
static and dynamic semantics of programming languages.
- Minimal models; fixed point proofs; Kripke models.
- Substructural logics: relevance, linear.