Logic began as the formal study of truth, reasoning, and provability. In computer science, it has become a fundamental language for specifying and analyzing computation: logical formulas can describe the behavior of programs, hardware, databases, and distributed systems, and they can also express the properties these systems are meant to satisfy. This course introduces the foundations behind these applications. Starting from propositional logic and first-order logic, we study the distinction between syntax and semantics, proof systems such as resolution, and the algorithmic questions that arise when logical statements are given as input. Which properties can be checked automatically? Which problems are efficiently solvable, and which are undecidable? By addressing questions such as satisfiability, validity, and finite-model reasoning, the course provides a first step toward more advanced topics in formal methods, model checking, automated reasoning, and formal verification.
