Logics for computer scientists*

General data

Course ID:	1000-217bLOG*
Erasmus code / ISCED:	11.304 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration The ISCED (International Standard Classification of Education) code has been designed by UNESCO.
Course title:	Logics for computer scientists*
Name in Polish:	Logika dla informatyków*
Organizational unit:	Faculty of Mathematics, Informatics, and Mechanics
Course groups:	Obligatory courses for 1st grade 2nd stage Computer Science
ECTS credit allocation (and other scores):	(not available) Basic information on ECTS credits allocation principles: the annual hourly workload of the student’s work required to achieve the expected learning outcomes for a given stage is 1500-1800h, corresponding to 60 ECTS; the student’s weekly hourly workload is 45 h; 1 ECTS point corresponds to 25-30 hours of student work needed to achieve the assumed learning outcomes; weekly student workload necessary to achieve the assumed learning outcomes allows to obtain 1.5 ECTS; work required to pass the course, which has been assigned 3 ECTS, constitutes 10% of the semester student load. view allocation of credits
Language:	English
Type of course:	obligatory courses
Short description:	Introduction to propositional logic and first-order logic: elements of model theory, elements of proof theory, the role of logic in informatics and computer science. Other logics that are significant in computer science.
Full description:	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).
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.
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 methods and 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.

This course is not currently offered.

Course descriptions are protected by copyright.
Copyright by University of Warsaw.