Logics for computer scientists*

General data

Course ID:	1000-217bLOG*
Erasmus code / ISCED:	11.304 The subject classification code consists of three to five digits, where the first three represent the classification of the discipline according to the Discipline code list applicable to the Socrates/Erasmus program, the fourth (usually 0) - possible further specification of discipline information, the fifth - the degree of subject determined based on the year of study for which the subject is intended. / (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.