Course detail
Introduction to Logic for Computer Science
FIT-IZLOAcad. year: 2022/2023
Formal propositional and predicate logic. Syntax and semantics of formulae. Normal forms and algebraic manipulation with formulae. Formal proof as a sequence of applications of syntactic rules originating in axioms. First order theories, models. Notions of correctness, soundness, completeness. Usage of SAT and SMT solvers. Connections of proving and computation, existence of their limits following from Gödel's theorems.
Language of instruction
Number of ECTS credits
Mode of study
Guarantor
Department
Learning outcomes of the course unit
Prerequisites
Co-requisites
Planned learning activities and teaching methods
Assesment methods and criteria linked to learning outcomes
Course curriculum
Work placements
Aims
Specification of controlled education, way of implementation and compensation for absences
Recommended optional programme components
Prerequisites and corequisites
- compulsory prerequisite
Discrete Mathematics
Basic literature
Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (CS)
Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/ (CS)
Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/ (EN)
Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (CS)
Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (EN)
Recommended reading
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
Elearning
Classification of course in study plans
Type of course unit
Lecture
Teacher / Lecturer
Syllabus
- Introduction, syntax and semantics of propositional logic, satisfiability, validity, truth tables, conjunctive and disjunctive normal form, algebraic manipulations with formulas, complete systems of connectives.
- Syntax and semantics of predicate logic.
- Normal forms and algebraic manipulation with predicate formulas. Theories in predicate logic.
- Formal proof. Proof from axioms by inference rules. The relation between syntax and semantics. Efficient, correct, complete proof systems.
- Soundness and completeness of first-order theories. The relation between computation and proof, mechanization of mathematics and PL theories, Gödel's incompleteness theorems.
Fundamentals seminar
Teacher / Lecturer
Syllabus
- SAT and SMT solving
Exercise
Teacher / Lecturer
Syllabus
- Propositional logic: formalization of statements, formula satisfaction, truth tables, conversions to CNF and DNF.
- Predicate logic: quantifiers and variables. Formalizing and understanding formulas 1.
- Predicate logic: language interpretation, models of formulas. Formalization and understanding formulas 2.
- Algebraic modifications and conversions to normal forms.
- Formal proof.
Project
Teacher / Lecturer
Syllabus
- Use of SAT solvers
- Use of SMT solvers
Elearning