Computational Logic

Introduction to logic. Propositional logic (syntax, semantics, Hilbert proof systems and Tableaux, validity and completeness). Predicate logic (syntax, semantics, Hilbert proof systems and Tableaux, validity, the completeness theorem for predicate logic). Elements of model theory. The incompleteness theorem and its consequences. Applications of logic in Computer Science: finite model theory and descriptive complexity (the use of logic in the characterization of complexity classes, Fagin’s theorem). The use of formal logic in the formal verification of software systems.