4 credits (3-0-2)
Pre-requisites: COL106 OR Equivalent
Overlaps with: MTL747
Review of the principle of mathematical induction; the principle of structural induction; review of Boolean algebras; Syntax of propositional formulas; Truth and the semantics of propositional logic; Notions of satisfiability, validity, inconsistency; Deduction systems for propositional logic; Completeness of deduction sytems; First order logic (FOL) ; Proof theory for FOL; introduction to model theory; completeness and compactness theorems; First order theories. Programming exercises will include representation and evalution; conversion to normal-forms; tautology checking; proof normalization; resolution; unification; Skolemization, conversion to Horn-clauses; binary-decision diagrams. Decidability, undecidability and complexity results. Introduction to formal methods, temporal/modal logics.