460-6002/01 – 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
YearSemesterwinter + summer
Study languageCzech
Year of introduction2010/2011Year 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
Combined 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ů.

E-learning

Další požadavky na studenta

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

Combined form (validity from: 2010/2011 Winter semester, validity until: 2012/2013 Summer semester)
Task nameType of taskMax. number of points
(act. for subtasks)
Min. number of points
Examination Examination  
Mandatory attendence parzicipation:

Show history

Occurrence in study plans

Academic yearProgrammeField of studySpec.FormStudy language Tut. centreYearWSType of duty
2019/2020 (P0613D140005) Computer Science P Czech Ostrava Choice-compulsory type B study plan
2019/2020 (P0541D170005) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory type B study plan
2019/2020 (P0541D170005) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory type B study plan
2019/2020 (P0613D140005) Computer Science K Czech Ostrava Choice-compulsory type B study plan
2019/2020 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2019/2020 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2019/2020 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2019/2020 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2018/2019 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2018/2019 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2018/2019 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2018/2019 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2017/2018 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2017/2018 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2017/2018 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2017/2018 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2016/2017 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2016/2017 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2016/2017 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2016/2017 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2015/2016 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2015/2016 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2015/2016 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2015/2016 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2014/2015 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2014/2015 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2014/2015 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2014/2015 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2014/2015 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K English Ostrava Choice-compulsory study plan
2013/2014 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2013/2014 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2013/2014 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2013/2014 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2012/2013 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2012/2013 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2012/2013 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2012/2013 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2011/2012 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2011/2012 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2011/2012 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2011/2012 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2010/2011 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2010/2011 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2010/2011 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics P Czech Ostrava Choice-compulsory study plan
2010/2011 (P1807) Computer Science, Communication Technology and Applied Mathematics (1801V001) Informatics K Czech Ostrava Choice-compulsory study plan
2010/2011 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2010/2011 (P1807) Computer Science, Communication Technology and Applied Mathematics (1103V036) Computational and Applied Mathematics K Czech Ostrava Choice-compulsory study plan

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner