Course detail

Introduction to Logic for Computer Science

FIT-IZLOAcad. year: 2023/2024

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

Czech

Number of ECTS credits

2

Mode of study

Not applicable.

Guarantor

doc. Mgr. Lukáš Holík, Ph.D.

Department

Department of Intelligent Systems (UITS)

Entry knowledge

Basics of discrete mathematics and its notation, sets, relations, functions.

Rules for evaluation and completion of the course

Evaluation of the project, which will consist of two homeworks: 1) use of SAT solver, 2) use of SMT solver.
The project is evaluated with a maximum of 18 points, the written exam with a maximum of 82 points. For successful completion of the course, you must obtain at least 50 points out of the 100 and also 40 points from the final exam.

Aims

Introduction to most basic concepts, terminology, and results of classical mathematical logic (syntax, semantics, formal proof in propositional and predicate logic); training of formal expression using the apparatus of mathematical logic; introduction to the connection with computing, formal reasoning, and their limits; introduction to the technology of automated logical reasoning—SAT and SMT solving.
Orientation in the notions of mathematical logic such as term, formula, axiom, proof, syntax, semantics, satisfiability, validity, correctness, soundness, axiom, proof. Familiarity with the language of propositional and predicate logic: thorough understanding of the meaning and usage of their symbols: connectives, quantifiers, logical variables. Ability to write and read texts with elements of formal notation. Improvement of overall ability to express oneself and to think formally and accurately. Basic knowledge of the most fundamental results in mathematical logic, Gödel's theorems, and their relevance to computer science. Awareness of the practical use of SAT and SMT solvers.

Study aids

Not applicable.

Prerequisites and corequisites

Basic literature

Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523 (CS)
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. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/ (CS)
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 (EN)
Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101 (EN)
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)
Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520 (EN)

Recommended reading

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)

eLearning

eLearning: currently opened course

Classification of course in study plans

  • Programme BIT Bachelor's, 1. year of study, summer semester, compulsory

  • Programme IT-BC-3 Bachelor's

    branch BIT , 1. year of study, summer semester, compulsory

  • Programme BIT Bachelor's, 1. year of study, summer semester, compulsory

Type of course unit

 

Lecture

10 hours, optionally

Teacher / Lecturer

doc. Mgr. Lukáš Holík, Ph.D.
Ing. Ondřej Lengál, Ph.D.

Syllabus

  1. Introduction, syntax and semantics of propositional logic, satisfiability, validity, truth tables, conjunctive and disjunctive normal form, algebraic manipulations with formulas, complete systems of connectives.
  2. Syntax and semantics of predicate logic.
  3. Normal forms and algebraic manipulation with predicate formulas. Theories in predicate logic.
  4. Formal proof. Proof from axioms by inference rules. The relation between syntax and semantics. Efficient, correct, complete proof systems.
  5. Soundness and completeness of first-order theories. The relation between computation and proof, mechanization of mathematics and PL theories, Gödel's incompleteness theorems.

Seminar

2 hours, optionally

Teacher / Lecturer

doc. Mgr. Lukáš Holík, Ph.D.

Syllabus

  1. SAT and SMT solving.

Exercise

10 hours, optionally

Teacher / Lecturer

Ing. Tomáš Dacík
doc. Mgr. Lukáš Holík, Ph.D.
Ing. Ondřej Lengál, Ph.D.
Mgr. Juraj Síč

Syllabus

  1. Propositional logic: formalization of statements, formula satisfaction, truth tables, conversions to CNF and DNF.
  2. Predicate logic: quantifiers and variables. Formalizing and understanding formulas 1.
  3. Predicate logic: language interpretation, models of formulas. Formalization and understanding formulas 2.
  4. Algebraic modifications and conversions to normal forms.
  5. Formal proof.

Project

2 hours, optionally

Teacher / Lecturer

Ing. Tomáš Dacík
doc. Mgr. Lukáš Holík, Ph.D.
Ing. Ondřej Lengál, Ph.D.
Mgr. Juraj Síč

Syllabus

  1. Use of SAT solvers
  2. Use of SMT solvers

eLearning

eLearning: currently opened course