456-0037/01 – Mathematical Logic (ML)

Gurantor departmentDepartment of Computer ScienceCredits8
Subject guarantorprof. RNDr. Marie Duží, CSc.Subject version guarantorprof. RNDr. Marie Duží, CSc.
Study levelundergraduate or graduateRequirementChoice-compulsory
YearSemesterwinter
Study languageCzech
Year of introduction1992/1993Year of cancellation2005/2006
Intended for the facultiesFEIIntended for study typesMaster
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 Credit and Examination 3+2

Subject aims expressed by acquired skills and competences

The course makes acquaintance with fundamentals of propositional and predicate calculus, clausular logic, Gentzen-like and Hilbert-like formal systems of logic, metamathematics as an informal theory of general formal systems.

Teaching methods

Lectures
Individual consultations
Tutorials

Summary

The course deals with fundamentals of mathematical logic and formal systems. It covers the following main topics: propositional and predicate calculus, clausular logic, Gentzen-like and Hilbert-like formal systems of logic, metamathematics as an informal theory of general formal systems.

Compulsory literature:

Duží, M.: [I]Matematická logika.[\I] Učební texty v elektronické podobě, VŠB-TU Ostrava, 2002. http:/www.cs.vsb.cz/duzi Švejdar, V.: [I]Logika (neúplnost, složitost, nutnost).[\I] Academia, Praha 2002. Sochor, A.: [I]Klasická matematická logika.[\I] Karolinum Praha, 2001. Kolář, J.-Štěpánková, O -Chytil, M.: Logika, algebra, grafy. Praha, SNTL 1989. Štěpán, J.: Formální logika. Olomouc, FIN 1995 Malina, J., Novotný, J. (ed.): Kurt Goedel. Brno, 1996. Lukasová, A.: Logické základy umělé inteligence, skripta PF Ostravské univerzity, 1999

Recommended literature:

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. Bibel, W.: Deduction (Automated Logic). Academia Press, 1993. Fitting, Melvin. First order logic and automated theorem proving [1996]. 2nd ed. New York : Springer, 1996. Graduate texts in computer science. .

Way of continuous check of knowledge in the course of semester

E-learning

Other requirements

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

Přednášky: Intuitivní (sémantický) výklad výrokové logiky založený na pojmu pravdivostní funkce. Jazyk výrokové logiky. Ekvivalence formulí výrokové logiky. Normální tvary formulí. Funkcionální úplnost systému pravdivostních funkcí. Systém přirozené dedukce výrokové logiky (Gentzen). Pojem důkazu v tomto systému. Axiomatický systém výrokové logiky. Pojem důkazu v tomto systému. Věta o dedukci a její důkaz. Postova věta a její důkaz. Automatické dokazování ve výrokové logice. Rezoluční odvozovací pravidlo a Robinsonův rezoluční princip. Intuitivní výklad predikátové logiky zaloľený na zobecnění výrokové logiky pro konečné universum předmětů. Jazyk predikátové logiky. Kanonické tvary formulí predikátové logiky. Prenexní tvar. Skolemizace. Systém přirozené dedukce predikátové logiky. Axiomatický systém predikátové logiky. Automatické dokazování v predikátové logice. Unifikace formulí a zobecnění rezolučního pravidla. Logické programy. Teorie formálních systémů (metateorie). Formalizované teorie a jejich modely. Definice nových pojmů ve formálních systémech. Vlastnosti formálních systémů. Bezespornost, úplnost, rozhodnutelnost, nezávislost axiómů, kategoričnost. Formalizovaná axiomatická teorie přirozených čísel. Formalizovaná axiomatická teorie množin.

Conditions for subject completion

Full-time form (validity from: 1960/1961 Summer semester)
Task nameType of taskMax. number of points
(act. for subtasks)
Min. number of pointsMax. počet pokusů
Exercises evaluation and Examination Credit and Examination 100 (145) 51 3
        Examination Examination 100  0 3
        Exercises evaluation Credit 45  0 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
2006/2007 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava 5 Optional study plan
2005/2006 (M2612) Electrical Engineering and Computer Science (2601T004) Measurement and Control Engineering P Czech Ostrava Choice-compulsory study plan
2005/2006 (M2612) Electrical Engineering and Computer Science (2612T018) Electronics and Communication Technology P Czech Ostrava Choice-compulsory study plan
2005/2006 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (10) Elektrické stroje a přístroje P Czech Ostrava Choice-compulsory study plan
2005/2006 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (20) Elektrické pohony a výkonová elektronika P Czech Ostrava Choice-compulsory study plan
2005/2006 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava Choice-compulsory study plan
2005/2006 (M2612) Electrical Engineering and Computer Science (3907T001) Electrical Power Engineering P Czech Ostrava Choice-compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava 3 Compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (2601T004) Measurement and Control Engineering P Czech Ostrava Choice-compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (2612T018) Electronics and Communication Technology P Czech Ostrava Choice-compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (10) Elektrické stroje a přístroje P Czech Ostrava Choice-compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (20) Elektrické pohony a výkonová elektronika P Czech Ostrava Choice-compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava Choice-compulsory study plan
2004/2005 (M2612) Electrical Engineering and Computer Science (3907T001) Electrical Power Engineering P Czech Ostrava Choice-compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava 3 Compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (2601T004) Measurement and Control Engineering P Czech Ostrava Choice-compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (2612T018) Electronics and Communication Technology P Czech Ostrava Choice-compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (10) Elektrické stroje a přístroje P Czech Ostrava Choice-compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (20) Elektrické pohony a výkonová elektronika P Czech Ostrava Choice-compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava Choice-compulsory study plan
2003/2004 (M2612) Electrical Engineering and Computer Science (3907T001) Electrical Power Engineering P Czech Ostrava Choice-compulsory study plan
2003/2004 (B2612) Electrical Engineering and Computer Science (1801R001) Computer Science P Czech Ostrava 3 Compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (2601T004) Measurement and Control Engineering P Czech Ostrava Choice-compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (2612T018) Electronics and Communication Technology P Czech Ostrava Choice-compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (10) Elektrické stroje a přístroje P Czech Ostrava Choice-compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (20) Elektrické pohony a výkonová elektronika P Czech Ostrava Choice-compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava Choice-compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (3907T001) Electrical Power Engineering P Czech Ostrava Choice-compulsory study plan
2002/2003 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava 3 Compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (2601T004) Measurement and Control Engineering P Czech Ostrava Choice-compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (2612T018) Electronics and Communication Technology P Czech Ostrava Choice-compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (10) Elektrické stroje a přístroje P Czech Ostrava Choice-compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (2642T004) Electrical Machines, Apparatus and Drives (20) Elektrické pohony a výkonová elektronika P Czech Ostrava Choice-compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava Choice-compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (3907T001) Electrical Power Engineering P Czech Ostrava Choice-compulsory study plan
2001/2002 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava 3 Compulsory study plan
2000/2001 (B2612) Electrical Engineering and Computer Science (1801R001) Computer Science P Czech Ostrava 3 Optional study plan
2000/2001 (M2612) Electrical Engineering and Computer Science (3902T023) Computer Science P Czech Ostrava 3 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í.