Logics for computer scientists* 1000-217bLOG*
1. Propositional logic: connections with logic circuits; proof systems; intuitionistic propositional logic.
2. Applications of propositional logic: SAT-solvers.
3. First-order logic: applications; connections with databases (Codd theorem); limitations of expressibility (Ehrenfeucht-Fraisse games); proof systems; completeness theorem.
4. Classical model theory: compactness theorem, Skolem-Loewenheim theorem.
5. Decidability of logical theories: undecidability of first-order logic; decidable fragments.
6. Arithmetic and Gödel incompleteness theorem.
7. Datalog as an extension of first-order logic with recursion.
8. Logic in verification of sequential and concurrent systems: SPIN, Coq, provers.
9. Second-order logic: SO, MSO and connections with automata, decidability, applications (for instance MONA).
Type of course
Learning outcomes
Knowledge:
1. Well-organized knowledge about syntax and semantics of first-order logic (K_W01, K_W02).
2. Knowledge about most important properties of first-order logic (K_W01, K_W02).
3. Basic knowledge about syntax and semantics of at least one logic relevant to computer science, other than first-order logic (K_W01, K_W02).
4. Knowledge about most important properties of of at least one logic relevant to computer science, other than first-order logic (K_W01, K_W02).
5. General knowledge about logical formalisms relevant to computer science (K_W01, K_W02).
6. Understanding of the role and importance of mathematical reasoning (K_W01, K_W02).
Skills
1. Is able to formalize properties in first-order logic (K_U09).
2. Can prove that certain properties can not be formalized in first-order logic (K_U09).
3. Is able to formalize simple properties in at least one logic relevant to computer science, other than first-order logic (K_U10).
4. Can prove that certain properties can not be formalized in at least one logic relevant to computer science, other than first-order logic (K_U10).
Competences
1. Is aware of the limitations of own knowledge and understands the need of further education, in particular outside of own domain (K_K01).
2. Is able to formulate precise questions, in the pursuit of deeper understanding and discovering missing elements of the argument (K_K02).
Assessment criteria
Tutorials result: the sum of points for solving homework problems and for a (noncompulsory) written test; homeworks alone suffice to get the maximal mark.
Exam result: sum of points awarded for solutions of problems.
Final result: weighted sum of the results of tutorials and exam.
Bibliography
Topics 1, 3, 4, 5, 6 from notes http://www.mimuw.edu.pl/~urzy/calosc.pdf
Topics 2, 7, 8, 9 from lecture slides.
Additional information
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: