Discrete mathematics: logical foundations of computing science [ LINGI1101 ]

• Elementary discrete mathematics (functions, sets, ...)
  
• Use of different techniques of mathematical proof

as provided by the courses FSAB1101, MAT1111 and SINF1250.

• 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.

Students completing successfully this course will be able to

• make good use of basic terminology for functions, relations and together and perform operations associated with these concepts in various concrete cases
  
• apply the formalism of propositional logic and predicate to model and reason about various real life situations
• describe the limitations and advantages of propositional logic and predicate logic, and choice the appropriate one for a given situation
• master different techniques of proof (direct proof, proof by counterexample, proof by contradiction, mathematical induction) to identify and apply the most appropriate in a particular situation
• exploit the link between on the one hand, mathematical induction and on the other hand, recursively defined structures and recursive programs in computer science to describe and reason about these programs and structures.

Students will have developed skills and operational methodology. In particular, they have developed their ability to

• interpret rigorously the concepts to understand in depth a written document or to write themselves a document,
• argue the use of rigor as a tool to avoid misinterpretation and detect errors in reasoning.

• short test during the semester
• written exam

• 2h of lecture / week
• 2h of exercise sessions / week

• 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.

• textbook available to the student printing service
• slides on icampus