Gurantor department | Department of Computer Science | Credits | 4 |

Subject guarantor | prof. RNDr. Marie Duží, CSc. | Subject version guarantor | prof. RNDr. Marie Duží, CSc. |

Study level | undergraduate or graduate | Requirement | Choice-compulsory |

Year | 1 | Semester | winter |

Study language | Czech | ||

Year of introduction | 2015/2016 | Year of cancellation | |

Intended for the faculties | FEI | Intended for study types | Follow-up Master |

Instruction secured by | |||
---|---|---|---|

Login | Name | Tuitor | Teacher giving lectures |

DUZ48 | prof. RNDr. Marie Duží, CSc. | ||

MEN059 | Mgr. Marek Menšík, Ph.D. |

Extent of instruction for forms of study | ||
---|---|---|

Form of study | Way of compl. | Extent |

Full-time | Credit and Examination | 2+2 |

Part-time | Credit and Examination | 10+0 |

The goal of the subject is to provide basic principles of logical proof calculi and axiomatic theories, and their application in the area of algebras and theory of lattices. A student should be able to exactly formulate and solve particular problems of computer science and applied mathematics.

Lectures

Seminars

Individual consultations

Tutorials

The course deals with fundamentals of mathematical logic and formal proof calculi. The following main topics are covered: propositional logic, 1st-order predicate logic, 1st-order proof calculi of Gentzen and Hilbert style and general resolution method. These methods are used in many areas of informatics in order to achieve a rigorous formalisation of intuitive theories (automatic theorem proving and deduction, artificial intelligence, and many others).

E. Mendelson. Introduction to Mathematical Logic, (4th edition). Chapman & Hall/CRC 1997.

Brown, J.R.: Philosophy of Mathematics. Routledge, 1999.
Thayse, A.: From Standard Logic to Logic Programming, John Wiley & Sons, 1988
Nerode, Anil - Shore, Richard A. Logic for applications. New York : Springer-Verlag, 1993. Texts and Monographs in Computer Science.
Richards, T.: Clausal Form Logic. An Introduction to the Logic of Computer Reasoning. Adison-Wesley, 1989.

Additional requirements are placed on the student.

Subject has no prerequisities.

Subject has no co-requisities.

Lectures:
1. Introduction: deductively valid arguments
2. Propositional logic: language (syntax and semantics)
3. Fuzzy logic
4. Proof methods in the propositional logic, resolution method
5. Naive set-theory; relation, function, countable/uncountable sets
6. First-order predicate logic (FOL): language (syntax and semantics)
7. Semantics of FOL language (interpretation and models)
8. Semantic tableaus in FOL
9. Aristotle logic. Venn's diagrams
10. General resolution method in FOL
11. Foundations of logic programming
12. Proof calculi, Natural deduction and sequent calculus
Seminars:
Deductively valid arguments
Propositional logic, language and semantics
Resolution method in propositional logic
Naive theory of sets
First-order predicate logic, language and semantics
Relation, function, countable and uncountable sets
Semantic tableau
Aristotelle logic
Resolution method in FOL
Logic programming
Proof calculi: natural deduction
Sequent calculus

Task name | Type of task | Max. number of points
(act. for subtasks) | Min. number of points |
---|---|---|---|

Credit and Examination | Credit and Examination | 100 (100) | 51 |

Credit | Credit | 40 (40) | 15 |

Credit test | Written test | 30 | 10 |

Online tests | Written test | 10 | 0 |

Examination | Examination | 60 (60) | 21 |

Test | Written examination | 40 | 21 |

Oral exam | Oral examination | 20 | 0 |

Show history

Academic year | Programme | Field of study | Spec. | Zaměření | Form | Study language | Tut. centre | Year | W | S | Type of duty | |
---|---|---|---|---|---|---|---|---|---|---|---|---|

2020/2021 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2020/2021 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2019/2020 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2019/2020 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2018/2019 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2018/2019 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2017/2018 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2017/2018 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2016/2017 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2016/2017 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2015/2016 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Choice-compulsory | study plan | ||||

2015/2016 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Choice-compulsory | study plan |

Block name | Academic year | Form of study | Study language | Year | W | S | Type of block | Block owner |
---|