Course details

# Introduction to Logic for Computer Science

IZLO Acad. year 2022/2023 Summer semester 2 credits

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.

Guarantor

Course coordinator

Language of instruction

Czech

Completion

Examination (written)

Time span

• 10 hrs lectures
• 12 hrs exercises
• 2 hrs projects

Assessment points

• 80 pts final exam
• 20 pts projects

Department

Lecturer

Instructor

Subject specific learning outcomes and competences

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.

Learning objectives

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.

Why is the course taught

The basic notions and concepts of mathematical logic were at the very beginning of computer science and permeate it at every step. They underlie logic circuits, processors, and almost every formal system or language, including programming languages, specification, and modeling. Becoming thoroughly familiar with basic notions of logic in their original form will help to navigate the derivative concepts of modern computer science.

Studying mathematical logic, the science of formal expression and reasoning, is also a unique opportunity to thoroughly practice precise expression and reasoning, a critical skill in any field of IT. A computer scientist constantly needs to assimilate, create, and communicate complex algorithms, models, systems, specifications, ...

SAT and SMT solving is an example of practical use of the theory taught. It is a versatile technology applicable in planning, arithmetic problem solving, graph problems, program analysis, testing, and verification, and other areas.

Finally, the basic facts about the connection between computing, formal reasoning, and mathematical proof, and the existence of their limits arising from Gödel's theorems, are among the most fundamental theoretical insights in computer science.

Prerequisites

Prerequisite knowledge and skills

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

Study literature

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

Fundamental literature

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

Syllabus of lectures

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.

Syllabus of exercises

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.

Syllabus of numerical exercises

1. SAT and SMT solving

Syllabus - others, projects and individual work of students

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

Progress assessment

Evaluation of the project, which will consist of two homeworks: 1) use of SAT solver, 2) use of SMT solver.

Controlled instruction

The project is evaluated with a maximum of 20 points, the written exam with a maximum of 80 points. For successful completion of the course, you must obtain at least 50 points out of the 100 and also half of the points from the final exam (i.e. 40 points of the 80).

Schedule

DayTypeWeeksRoomStartEndCapacityLect.grpGroupsInfo
Mon exam 2023-05-22 D0206 D0207 D105 09:0010:501. oprava
Mon exercise *) 2023-02-06 A113 D0207 09:0010:509999 1BIA 1BIB 2BIA 2BIB xx
Mon exam 2023-05-15 D0206 D0207 D105 E112 14:0015:50řádná
Mon exercise 2., 6., 8. of lectures G202 15:0016:5053 1BIA 1BIB 2BIA 2BIB xx Lengál
Mon exercise 2023-02-27 G202 15:0016:5053 1BIA 1BIB 2BIA 2BIB xx Holík
Mon lecture 1., 3., 5. of lectures D0206 D105 17:0018:509999 1BIA 2BIA 2BIB xx 10 - 29 Lengál
Mon lecture 7., 9., 11. of lectures D0206 D105 17:0018:509999 1BIA 2BIA 2BIB xx 10 - 29 Holík
Tue exercise 2., 4., 6., 8. of lectures A113 08:0009:5050 1BIA 1BIB 2BIA 2BIB xx Lengál
Tue exercise 2., 4., 6., 8. of lectures D0207 08:0009:5050 1BIA 1BIB 2BIA 2BIB xx Holík
Tue exercise 2., 4., 6., 8. of lectures D0206 11:0012:5053 1BIA 1BIB 2BIA 2BIB xx Holík
Tue exercise 2., 4., 6., 8. of lectures D0207 16:0017:5052 1BIA 1BIB 2BIA 2BIB xx Dacík
Tue exercise 2., 4., 6., 8. of lectures D0207 18:0019:5051 1BIA 1BIB 2BIA 2BIB xx Dacík
Wed exercise 2., 4., 6., 8. of lectures G202 14:0015:5053 1BIA 1BIB 2BIA 2BIB xx Dacík
Wed exercise 2., 4., 6., 8. of lectures G202 16:0017:5050 1BIA 1BIB 2BIA 2BIB xx Dacík
Thu exercise 2., 4., 6., 8. of lectures D0207 08:0009:5051 1BIA 1BIB 2BIA 2BIB xx Síč
Thu exercise 2., 4., 6., 8. of lectures G202 10:0011:5050 1BIA 1BIB 2BIA 2BIB xx Síč
Fri exercise 2., 4. of lectures D0207 08:0009:5070 1BIA 1BIB 2BIA 2BIB xx Lengál
Fri exercise 7., 8. of lectures D0207 08:0009:5070 1BIA 1BIB 2BIA 2BIB xx Síč
Fri exercise *) 2023-02-17 G202 08:0009:5050 1BIA 1BIB 2BIA 2BIB xx Síč
Fri exam 2023-05-05 D0206 D105 10:0011:50předtermín
Fri lecture 1., 3., 5. of lectures D0206 D105 10:0011:509999 1BIB 2BIA 2BIB xx 30 - 49 Lengál
Fri lecture 7., 10., 11. of lectures D0206 D105 10:0011:509999 1BIB 2BIA 2BIB xx 30 - 49 Holík
Fri exercise 2., 4., 7., 8. of lectures D0207 12:0013:5050 1BIA 1BIB 2BIA 2BIB xx Holík
Fri exercise 2., 7., 8. of lectures G202 12:0013:5050 1BIA 1BIB 2BIA 2BIB xx Síč
Fri exercise 2023-03-03 G202 12:0013:5050 1BIA 1BIB 2BIA 2BIB xx Lengál
Fri exam 2023-06-02 D0206 D0207 D105 E112 15:0016:502. oprava
It is not possible to register this class in Studis. (Some exercises may be opened later if needed, but this is not guaranteed.)

Course inclusion in study plans

• Programme BIT, 1st year of study, Compulsory
• Programme BIT (in English), 1st year of study, Compulsory
• Programme IT-BC-3, field BIT, 1st year of study, Compulsory
Back to top