|
|
|
 |
Logic and Computation |
| |
|
18h L / 6h R / 1WE / 2 ECTS credits / IIC_LRR |
| |
|
Didier GALMICHE |
| |
|
The aim of this course is to study the relationships between logic, computation models and some programming paradigms. We study the first-order logic both from proof theory and semantics or model theory perspectives. We consider the foundations of logic programming (resolution) and of functional programming (reduction) from (typed) lambda-calculus. Some non-standard logics (intuitionistic and modal logics) are considered in the context of modelling and verification.
|
| |
|
Logic and languages |
| |
|
Truth (models) and provability (proofs). Goedel theorem and its consequences.
Formal systems (sequent calculi, natural deduction), classical logic and intuitionistic logic, links between logic and languages
(propositions-as-types). Curry-Howard isomorphism.
|
| |
|
Functions and computations (reduction) |
| |
|
Lambda-calculus: introduction, formal system, operational semantics (reduction), properties (Church-Rosser, normalisation). Representation in lambda-calculus, extensionality, non-decidability, denotational semantics.
Typed lambda-calculus: types, type inference, strong normalisation, type systems, functional programming.
|
| |
|
Logic and computations (resolution) |
| |
|
Propositional logic, predicate logic, semantics and axiomatisation.
Formal systems and proofs: calculi à la Hilbert, sequent calculi, natural deduction, tableaux method.
Formula transformations, clauses, Herbrand theorem.
Resolution, strategies, logic programming.
Non-standard logics and applications (modelling and verification).
|
| |
| |
| |
| |
|
References
R. David, K. Nour, C. Raffali, Introduction à la Logique (théorie de la démonstration), Dunod.
J.Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, Cambridge University Press (Tracts in TCS).
|
| |
| |
| Last update 05/07/2007 by Cl.M. |
|
