Aims

- To acquire the mathematical foundations of a variety of concepts and techniques used in computing science.

- To make the appropriate connections between such foundations and various application domains in programming, data structures, artificial intelligence, software engineering, databases, robotics, etc.).

- To apply rigorous approaches for formalizing structures found in computing science and for reasoning about such structures.

Main themes

- Introduction to mathematical logic: propositional logic, predicate logic; first-order theories.

- Reasoning mechanisms: resolution, rewriting, induction on well-founded sets.

- Discrete structures as first-order theories: equality, partial orders, lattices; nonnegative integers, tuples, lists, trees, sets, multisets, sequences, etc.

Content and teaching methods

- Preliminaries: sets, relations, and functions; formal systems.

- Mathematical logic: proposition calculus -- syntax, semantics, proof theory; first-order predicate calculus -- syntax, semantics, proof theory ; resolution and refutation; first-order theories --models, consistency, inclusion, extension, etc.

- Equational theories: equality, partial orders, lattices, groups.

- Inductive theories: well-founded relations and the general induction principle. Basic inductive theories : nonnegative integers, tuples, lists, trees, sets, multisets, sequences, etc. Structure generators, systematic construction of axiomatisations, and inductive proofs of typical properties according to various induction rules (recurrence, complete induction, etc.).

Applications to various domains : program verification, specification of abstract data types, automated reasoning, expert systems, robotics, databases, parsing, etc.

Implementation with declarative programming languages such as PROLOG or ML.

Other information (prerequisite, evaluation (assessment methods), course materials recommended readings, ...)

- Weekly exercise sessions require students to come prepared and be actively involved -questions/answers, and resolution, by small groups, of problems submitted during the previous week. Quizzes are organized regularly to make sure that students follow and work properly.

- Prerequisite:
Elementary maths (assumed to be acquired after the first two bachelor years).

- References:
(1) Course lecture notes (available at " SICI ").

(2) Z. Manna and R. Waldinger, The Deductive Foundations of Computer Programming, Addison-Wesley, 1993.

(3) D. Gries, F. Schneider, A Logical Approach to Discrete Mathematics, Springer-Verlag, 1994.

- Evaluation :
Quizzes throughout the quadrimester, and written exam at the end.

Programmes in which this activity is taught

Other credits in programs