456-0904/01 – 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 introduction1997/1998Year of cancellation2010/2011
Intended for the facultiesFEIIntended for study typesDoctoral
Instruction secured by
LoginNameTuitorTeacher giving lectures
JAN59 prof. RNDr. Petr Jančar, CSc.
Extent of instruction for forms of study
Form of studyWay of compl.Extent
Full-time Credit and Examination 3+0
Part-time Credit and Examination 3+0

Subject aims expressed by acquired skills and competences

Teaching methods

Summary

The course deals with fundamentals of mathematical logic. It covers the following main topics: First order logic, modal logic, temporal logic, logical programing, godel theorem.

Compulsory literature:

Recommended literature:

Way of continuous check of knowledge in the course of semester

E-learning

Další požadavky na studenta

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

Přednášky: Hierarchie logik. Logika 1.řádu. Pojem formule a definice jazyka logiky 1.řádu. Sémantický výklad logiky 1.řádu. Relace definované na množině formulí /sémantická ekvivalence a vyplývání/. Kanonické tvary formulí: prenexní tvar, skolemizace. Gentzenovské systémy přirozené dedukce logiky 1.řádu. Axiomatické systémy logiky 1.řádu. Věty o dedukci, korektnosti a sémantické úplnosti. Automatické dokazování: rezoluce, unifikace, Robinsonův princip, logické programy. Reprezentace znalostí a logické vyvozování. Modální logiky. Temporální logika. Metamatematika jako teorie formálních systémů. Definice pojmů uvnitř formálních systémů. Vlastnosti formálních systémů: bezespornost, úplnost, rozhodnutelnost, kategoričnost, nezávislost axiómů. Formalizovaná teorie přirozených čísel a množin. Omezené možnosti formalizace. Gödelovy věty.

Conditions for subject completion

Full-time form (validity from: 1960/1961 Summer semester, validity until: 2012/2013 Summer semester)
Task nameType of taskMax. number of points
(act. for subtasks)
Min. number of points
Exercises evaluation and Examination Credit and Examination 100 (145) 51
        Examination Examination 100  0
        Exercises evaluation Credit 45  0
Mandatory attendence parzicipation:

Show history

Occurrence in study plans

Academic yearProgrammeField of studySpec.ZaměřeníFormStudy language Tut. centreYearWSType of duty
2009/2010 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2009/2010 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2008/2009 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2008/2009 (P2646) Information Technology K Czech Ostrava Choice-compulsory study plan
2008/2009 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics K Czech Ostrava Choice-compulsory study plan
2007/2008 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2006/2007 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2005/2006 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2004/2005 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2003/2004 (P2646) Information Technology (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2002/2003 (P2612) Electrical Engineering and Computer Science (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan
2001/2002 (P2612) Electrical Engineering and Computer Science (1801V002) Computer Science and Applied Mathematics P Czech Ostrava Choice-compulsory study plan

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner