460-4004/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 graduateRequirementOptional
YearSemesterwinter
Study languageCzech
Year of introduction2010/2011Year of cancellation2014/2015
Intended for the facultiesFEIIntended for study typesFollow-up Master
Instruction secured by
LoginNameTuitorTeacher giving lectures
SNE10 Mgr. Pavla Dráždilová, Ph.D.
DUZ48 prof. RNDr. Marie Duží, CSc.
JAR148 Ing. Vladimír Jarotek
KOJ0004 Ing. Lumír Kojecký, Ph.D.
MEN059 Mgr. Marek Menšík, Ph.D.
PAL350 Ing. Břetislav Paláček
Extent of instruction for forms of study
Form of studyWay of compl.Extent
Full-time Credit and Examination 3+3
Part-time Credit and Examination 10+10

Subject aims expressed by acquired skills and competences

The goal of the subject is to provide basic principles of logical proof calculi and axiomatic theories, and their application in the area of algebras and theory of lattices. A student should be able to exactly formulate and solve particular problems of computer science and applied mathematics.

Teaching methods

Lectures
Seminars
Individual consultations
Tutorials

Summary

The course deals with fundamentals of mathematical logic and formal proof calculi. The following main topics are covered: propositional logic, 1st-order predicate logic, 1st-order proof calculi of Gentzen and Hilbert style and general resolution method. These methods are used in many areas of informatics in order to achieve a rigorous formalisation of intuitive theories (automatic theorem proving and deduction, artificial intelligence, and many others).

Compulsory literature:

M.Duží: Mathematical logic. http://www.cs.vsb.cz/duzi/Mat-logika.html Z. Manna: Mathematical theory of Computer Science. McGraw-Hill, 1974.

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

Conditions for credit: Two written tests, each of which max. 15 grades. Maximum grades is thus 30. Minimum to obtain accreditation 14 grades, that is at least 7 grades from each test.

E-learning

Other requirements

Additional requirements are placed on the student.

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

Lectures: 1. Introduction: deductively valid arguments 2. Propositional logic: language (syntax and semantics) 3. Proof methods in the propositional logic, resolution method 4. Naive set-theory; relation, function, countable/uncountable sets 5. First-order predicate logic (FOL): language (syntax and semantics) 6. Semantics of FOL language (interpretation and models) 7. Semantic tableaus in FOL 8. Aristotle logic. Venn's diagrams 9. General resolution method in FOL 10. Foundations of logic programming 11. Proof calculi 12. Natural deduction Exercises: Deductively valid arguments Propositional logic, language and semantics Resolution method in propositional logic Naive theory of sets First-order predicate logic, language and semantics Relation, function, countable and uncountable sets Semantic tableau Aristotelle logic Resolution method in FOL Proof calculi: natural deduction

Conditions for subject completion

Full-time form (validity from: 2010/2011 Winter semester, validity until: 2012/2013 Winter 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 (100) 51
        Exercises evaluation Credit 30 (30) 14
                1. zápočtový test Written test 15  7
                2. zápočtový test Written test 15  7
        Examination Examination 70 (70) 37 3
                Písemný test Written examination 40  21
                Ústní zkouška Oral examination 30  16
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
2014/2015 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2014/2015 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Optional study plan
2014/2015 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2014/2015 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Optional study plan
2013/2014 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2013/2014 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2013/2014 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Optional study plan
2013/2014 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Optional study plan
2012/2013 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2012/2013 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2012/2013 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Optional study plan
2012/2013 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Optional study plan
2011/2012 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2011/2012 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2011/2012 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Choice-compulsory study plan
2011/2012 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Choice-compulsory study plan
2010/2011 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2010/2011 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2010/2011 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Choice-compulsory study plan
2010/2011 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Choice-compulsory study plan
2010/2011 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (2601R004) Measurement and Control Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (2602R014) Applied and Commercial Electronics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (3901R039) Biomedical Technician (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (3907R001) Electrical Power Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (1103R031) Computational Mathematics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (2601R013) Telecommunication Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (2612R025) Computer Science and Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (2612R059) Mobile Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2647) Information and Communication Technology (1103T031) Computational Mathematics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2647) Information and Communication Technology (2601T013) Telecommunication Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2647) Information and Communication Technology (2612T059) Mobile Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (2601T004) Measurement and Control Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (2612T015) Electronics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (3901T009) Biomedical Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (3907T001) Electrical Power Engineering (01) Exchange Students P Czech Ostrava Optional study plan

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner
V - ECTS - mgr. 2014/2015 Full-time Czech Optional 401 - Study Office stu. block
V - ECTS - mgr. 2013/2014 Full-time Czech Optional 401 - Study Office stu. block
V - ECTS - mgr. 2012/2013 Full-time Czech Optional 401 - Study Office stu. block
V - ECTS - mgr. 2011/2012 Full-time Czech Optional 401 - Study Office stu. block

Assessment of instruction



2014/2015 Winter
2013/2014 Winter
2012/2013 Winter
2011/2012 Winter
2010/2011 Winter