COMP 426: Automated Reasoning

- Twelf examples for encoding propositions and natural deduction twelf code

- SML code for proof checker sml

Fall 2007

Time: MWF 10:35-11:25

Location: Trottier 0070

Logic provides computer science with both a unifying foundational framework and a tool for modeling. In fact, logic has been called "the calculus of computer science", playing a crucial role in diverse areas such as artificial intelligence, computational complexity, distributed computing, database systems, hardware design, programming languages, and software engineering This course is designed to provide a thorough introduction to modern constructive logic, its numerous applications in computer science, and its mathematical properties. Some of the topics to be covered are intuitionistic logic, functional and logic programming, type theory, theorem proving, unification, first-order logic, non-classical logics.

If you are interested, send me e-mail (bp at cs.mcgill.ca).

**Theme of this course**

``On theories such as these we cannot rely. Proof we need. Proof!" -- Yoda, Jedi Master

**Prerequisites:**:
This is an upper-level undergraduate course. The prerequisites is COMP 302.

If you are a graduate student interested in this course, please contact me.