456-0349/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
Year1Semesterwinter
Study languageCzech
Year of introduction2006/2007Year of cancellation2009/2010
Intended for the facultiesFEIIntended for study typesFollow-up Master
Instruction secured by
LoginNameTuitorTeacher giving lectures
CIH053 PhDr. Martina Číhalová, Ph.D.
CIP016 Ing. Nikola Ciprich
SNE10 Mgr. Pavla Dráždilová, Ph.D.
DUZ48 prof. RNDr. Marie Duží, CSc.
FRY057 Ing. Tomáš Frydrych
MEN059 Mgr. Marek Menšík, Ph.D.
Extent of instruction for forms of study
Form of studyWay of compl.Extent
Full-time Credit and Examination 4+4
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
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: Three written tests, each of which max. 10 grades. Maximum grades is thus 30. Minimum to obtain accreditation 15 grades.

E-learning

Other requirements

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

Lectures: The notion of relation: Homogeneous and heterogeneous relations. Binary relations and their types. Reflexivity, ireflexivity, symmetry, antisymmetry, asymmetry, tranzitivity. Mapping as a special type of relation. Complete, total, partial mapping. Surjection, injection, bijection. Semantic exposition of propositional and 1st-order predicate logic. Basic principles of logical calculi and theories. The notion of a proof, axiom and theorem. Rezolution method of proving logical validity and validity of an argument. Robinson's unification algorithm. Logical programming. The natural deduction system (Gentzen). Proof in the system. Soundness and completeness. Hilbert-like proof calculus. The notion of a proof in the calculus. Theorem of deduction, soundness and completeness. Axiomatic theories and their properties. The set theory, relational and algebraic theories. Robinson and Peano arithmetic. (In)completeness, decidability, models. Gödel theorems and their importance in computer science. Closure of a relation, equivalence, factor set. Ordering Relations (partial, complete, quasi-ordering, linear). General notion of an operation. Algebras and their morphisms. Fundamentals of the lattice theory. Exercises: Deductively valid arguments Naive theory of sets Propositional logic, language and semantics Resolution method in propositional logic First-order predicate logic, language and semantics Relation, function, countable and uncountable sets Semantic tableau Aristotelova logika Resolution method in 1st-order predicate logic Proof calculi: natural deduction and Hilbert calculus Theory of relations, functions, algebras Projects: Solving a given problem by natural deduction and resolution methods

Conditions for subject completion

Conditions for completion are defined only for particular subject version and form of study

Occurrence in study plans

Academic yearProgrammeBranch/spec.Spec.ZaměřeníFormStudy language Tut. centreYearWSType of duty
2009/2010 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2009/2010 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Choice-compulsory study plan
2009/2010 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2009/2010 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Choice-compulsory study plan
2008/2009 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2008/2009 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2008/2009 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Choice-compulsory study plan
2008/2009 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Choice-compulsory study plan
2007/2008 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2007/2008 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2007/2008 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Choice-compulsory study plan
2007/2008 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Choice-compulsory study plan
2006/2007 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2006/2007 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2006/2007 (N2647) Information and Communication Technology (2612T059) Mobile Technology P Czech Ostrava 1 Choice-compulsory study plan
2006/2007 (N2647) Information and Communication Technology (2612T059) Mobile Technology K Czech Ostrava 1 Choice-compulsory study plan

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner

Assessment of instruction



2009/2010 Winter