The course will first introduce some notation and tools in the field of formal logic and deductive reasoning, such as truth tables, logic conjunctions, and implications. Then, it will explore how these tools can be exploited to establish the validity of certain statements and facts, discussing the proof techniques based on deduction and on contradiction.
The next goal will be to discuss certain structures in discrete mathematics that are heavily used in computer science and to study their combinatorial properties. This includes integer numbers, with their binary representation in a computer, permutations, sequences, and series, together with elements of set theory and of graph theory. Using these structures as training fields for various examples, another powerful proof technique, based on mathematical induction, will be introduced.
Finally, the course will overview some state-of-the-art algorithmic solutions for fundamental computer science problems, such as searching and sorting, and use the techniques learned in the course to formally prove their correctness. To further establish the efficiency of these solutions, basic principles of computational complexity will be presented, including recurrences, counting arguments, and asymptotic notation.
To provide students with a direct research experience, each of them will be assigned a theorem from a research paper, whose statement and proof will be presented and discussed in class.