Logic and Foundations of Computer Science

Course Objectives

The objectives of this module are twofold:

  1. To introduce students to mathematical logic, particularly proof theory.

  2. To provide students with the necessary foundations to understand how most automated theorem-proving tools operate—especially those developed in academic environments—and potentially to design and implement such tools themselves.

This course is essential for students who intend to pursue research in areas such as formal verification, automated theorem proving, or term rewriting. It is also highly relevant to related fields including computer systems security, embedded systems, proof assistants, and, more broadly, the use of formal methods in computer science.

To achieve these objectives, the course proposes the study of at least one of the following logical systems:

  • First-Order Logic, widely used for formalization and reasoning in fields such as Artificial Intelligence and Databases.

  • Equational Logic, useful for the specification and verification of sequential programs.

  • Intuitionistic Logic, which provides constructive proofs and forms the theoretical basis for many automated reasoning techniques.