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

**recommended prerequisite**

Discrete Mathematics

Basic literature

Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520 (EN)

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/ (EN)

Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (CS)

Recommended reading

Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)

Elearning

**eLearning:**currently opened course

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

**eLearning:**currently opened course