460-6002/02 – Theory of Formal Systems (TFS)

Gurantor departmentDepartment of Computer ScienceCredits10
Subject guarantorprof. RNDr. Marie Duží, CSc.Subject version guarantorprof. RNDr. Marie Duží, CSc.
Study levelpostgraduateRequirementChoice-compulsory type B
YearSemesterwinter + summer
Study languageEnglish
Year of introduction2015/2016Year of cancellation
Intended for the facultiesFEIIntended for study typesDoctoral
Instruction secured by
LoginNameTuitorTeacher giving lectures
DUZ48 prof. RNDr. Marie Duží, CSc.
Extent of instruction for forms of study
Form of studyWay of compl.Extent
Full-time Examination 28+0
Part-time Examination 28+0

Subject aims expressed by acquired skills and competences

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.

Teaching methods

Seminars
Individual consultations

Summary

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.

Compulsory literature:

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

Recommended literature:

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,

Way of continuous check of knowledge in the course of semester

Schopnost samostatného studia doporučených pramenů. Ústní zkouška

E-learning

Other requirements

There are not defined other requirements for student.

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

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

Conditions for subject completion

Full-time form (validity from: 2015/2016 Winter semester)
Task nameType of taskMax. number of points
(act. for subtasks)
Min. number of pointsMax. počet pokusů
Examination Examination   3
Mandatory attendence participation:

Show history

Conditions for subject completion and attendance at the exercises within ISP:

Show history

Occurrence in study plans

Academic yearProgrammeBranch/spec.Spec.ZaměřeníFormStudy language Tut. centreYearWSType of duty
2023/2024 (P0613D140033) Informatics and Computational Science K English Ostrava Choice-compulsory type B study plan
2023/2024 (P0613D140033) Informatics and Computational Science P English Ostrava Choice-compulsory type B study plan
2023/2024 (P0541D170006) Computational and Applied Mathematics K English Ostrava Choice-compulsory type B study plan
2023/2024 (P0541D170006) Computational and Applied Mathematics P English Ostrava Choice-compulsory type B study plan
2023/2024 (P0613D140006) Computer Science K English Ostrava Choice-compulsory type B study plan
2023/2024 (P0613D140006) Computer Science P English Ostrava Choice-compulsory type B study plan
2023/2024 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P English Ostrava Choice-compulsory study plan
2023/2024 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K English Ostrava Choice-compulsory study plan
2023/2024 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P English Ostrava Choice-compulsory study plan
2023/2024 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K English Ostrava Choice-compulsory study plan
2022/2023 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P English Ostrava Choice-compulsory study plan
2022/2023 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K English Ostrava Choice-compulsory study plan
2022/2023 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P English Ostrava Choice-compulsory study plan
2022/2023 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K English Ostrava Choice-compulsory study plan
2022/2023 (P0613D140006) Computer Science P English Ostrava Choice-compulsory type B study plan
2022/2023 (P0613D140006) Computer Science K English Ostrava Choice-compulsory type B study plan
2022/2023 (P0541D170006) Computational and Applied Mathematics K English Ostrava Choice-compulsory type B study plan
2022/2023 (P0541D170006) Computational and Applied Mathematics P English Ostrava Choice-compulsory type B study plan
2022/2023 (P0613D140033) Informatics and Computational Science P English Ostrava Choice-compulsory type B study plan
2022/2023 (P0613D140033) Informatics and Computational Science K English Ostrava Choice-compulsory type B study plan
2021/2022 (P0541D170006) Computational and Applied Mathematics P English Ostrava Choice-compulsory type B study plan
2021/2022 (P0541D170006) Computational and Applied Mathematics K English Ostrava Choice-compulsory type B study plan
2021/2022 (P0613D140006) Computer Science K English Ostrava Choice-compulsory type B study plan
2021/2022 (P0613D140006) Computer Science P English Ostrava Choice-compulsory type B study plan
2021/2022 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P English Ostrava Choice-compulsory study plan
2021/2022 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K English Ostrava Choice-compulsory study plan
2021/2022 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P English Ostrava Choice-compulsory study plan
2021/2022 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K English Ostrava Choice-compulsory study plan
2020/2021 (P0541D170006) Computational and Applied Mathematics P English Ostrava Choice-compulsory type B study plan
2020/2021 (P0541D170006) Computational and Applied Mathematics K English Ostrava Choice-compulsory type B study plan
2020/2021 (P0613D140006) Computer Science P English Ostrava Choice-compulsory type B study plan
2020/2021 (P0613D140006) Computer Science K English Ostrava Choice-compulsory type B study plan
2020/2021 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P English Ostrava Choice-compulsory study plan
2020/2021 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K English Ostrava Choice-compulsory study plan
2020/2021 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P English Ostrava Choice-compulsory study plan
2020/2021 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K English Ostrava Choice-compulsory study plan
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

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner

Assessment of instruction

Předmět neobsahuje žádné hodnocení.