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

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

Study level | postgraduate | Requirement | Choice-compulsory type B |

Year | Semester | winter + summer | |

Study language | English | ||

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

Intended for the faculties | FEI | Intended for study types | Doctoral |

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

Login | Name | Tuitor | Teacher giving lectures |

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

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

Form of study | Way of compl. | Extent |

Full-time | Examination | 28+0 |

Part-time | Examination | 28+0 |

The course provides an exposition of the apparatus and proof methods of the first-order predicate logic (FOL), in particular proof calculi and theories based on FOL. These formal frameworks are applied in many areas of computer science such as a formal specification of information systems, automated proving and inference machines, query languages, declarative programming programming, and in general in artificial intelligence.

Seminars

Individual consultations

This course is a summary and an extension of the course on Mathematical Logic that is being offered to undergraduate students. Unlike the latter that concentrates on pure mathematical logtic, the former gives a greater saliency to formal proof calculi and theories, in particular their application in computer science. Students obtain information on theories applied in knowledge-based systems, artificial intelligence, multi-agent systems and other disciplines of computer science.

A.Thayse et al.: From standard logic to logic programming /Introducing a logic based approach to arificial intelligence/. John Wiley and Sons, 1989

T Richards: Clausal form logic /An Introduction to the logic of computer reasoning/ Addison-Wesley, 1989
W.Bibel: Deduction /Automated Logic/. Academic Press, San Diego, 1993
Nerode, Anil - Shore, Richard A. Logic for applications. New York : Springer-Verlag, 1993. Texts and Monographs in Computer Science.
Fitting, Melvin. First order logic and automated theorem proving [1996]. 2nd ed. New York : Springer, Graduate texts in computer science.
F.Kroeger: Temporal Logic of Programs. Springer-Verlag,

Schopnost samostatného studia doporučených pramenů.

There are not defined other requirements for student.

Subject has no prerequisities.

Subject has no co-requisities.

Proof calculi;
Natural deduction;
Sequent calculus
Hilbert kalkul;
Axiomatic theories of relations; ordering and equivalence
Axiomatic theory of functions; mapping, isomorphisms and homomorphisms
Algebraic teories; groups, fields
Theory of lattices; relational vs. algebraic
Theories of arithmetic, Gödel's theorems on incompleteness

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

Examination | Examination |

Show history

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

2019/2020 | (P0613D140006) Computer Science | P | English | Ostrava | Choice-compulsory type B | study plan | ||||||

2019/2020 | (P0541D170006) Computational and Applied Mathematics | P | English | Ostrava | Choice-compulsory type B | study plan | ||||||

2019/2020 | (P0541D170006) Computational and Applied Mathematics | K | English | Ostrava | Choice-compulsory type B | study plan | ||||||

2019/2020 | (P0613D140006) Computer Science | K | English | Ostrava | Choice-compulsory type B | study plan | ||||||

2019/2020 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2019/2020 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2019/2020 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2019/2020 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2018/2019 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2018/2019 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2018/2019 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2018/2019 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2017/2018 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2017/2018 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2017/2018 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2017/2018 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2016/2017 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2016/2017 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2016/2017 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2016/2017 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2015/2016 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2015/2016 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1103V036) Computational and Applied Mathematics | K | English | Ostrava | Choice-compulsory | study plan | |||||

2015/2016 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | P | English | Ostrava | Choice-compulsory | study plan | |||||

2015/2016 | (P1807) Computer Science, Communication Technology and Applied Mathematics | (1801V001) Informatics | K | English | Ostrava | Choice-compulsory | study plan |

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