The aim of this course is twofold:
- To introduce students to mathematical logic, with a particular focus on proof theory.
- To provide students with the necessary foundations to understand how automated theorem proving tools work, especially those developed in academic research, and possibly enable them to design and implement such tools.
This course is essential for students intending to pursue research in areas such as formal verification, automated theorem proving, term rewriting systems, and related fields. It is also relevant for domains such as computer system security, embedded systems, proof assistants, and the general use of formal methods.
To achieve these objectives, the course may be based on one or more of the following logical systems:
- First-order logic (widely used in artificial intelligence and database systems)
- Equational logic (useful for specification and verification of sequential programs)
- Intuitionistic logic (focused on constructive proofs and foundations of automated reasoning)
- Teacher: Nour El Houda Sayah Ben Aissa