456-0317/01 – Mathematical Foundations of Informatics (MZI)
Gurantor department | Department of Computer Science | Credits | 8 |
Subject guarantor | prof. RNDr. Marie Duží, CSc. | Subject version guarantor | prof. RNDr. Marie Duží, CSc. |
Study level | undergraduate or graduate | Requirement | Compulsory |
Year | 2 | Semester | winter |
| | Study language | Czech |
Year of introduction | 2003/2004 | Year of cancellation | 2009/2010 |
Intended for the faculties | FEI | Intended for study types | Follow-up Master |
Subject aims expressed by acquired skills and competences
The goal of the subject is to provide basic principles of logical proof calculae and axiomatic theories, and their application in the area of algebras and theory of lattices. The student should be able to exactly formulate and solve particular problems of computer science and applied mathematics.
Teaching methods
Summary
The course is oriented to basic principles of formal logical calculae and axiomatic theories, in particular algebraic theories. Practical applicability of this rigid logical view-point in informatics is stressed.
Compulsory literature:
M. Duzi: Mathematical Logic and Proof Calculi. Retrivable at: http://www.cs.vsb.cz/duzi/mzi.html
M. Duzi: Goedel's Results on Completeness and Incompleteness.
Retrivable at: http://www.cs.vsb.cz/duzi/mzi.html
Recommended literature:
Sochor, A.: Klasická matematická logika. Karolinum Praha, 2001.
Švejdar, V.: Logika, neúplnost a složitost. Academia Praha, 2002.
Way of continuous check of knowledge in the course of semester
Conditions for credit:
Solving a given problem during the semester (max. 10 grades).
Presentation of the problem solution (voluntary - bonus 5 grades).
Written test maximum 15 points.
Minimum to obtain accreditation 12 grades.
E-learning
Other requirements
Prerequisities
Subject has no prerequisities.
Co-requisities
Subject has no co-requisities.
Subject syllabus:
Lectures:
Naive set theory: operations on sets, relations between sets, and definition of these in terms of the 1st order predicate logic (FOL).
Cartezian product, relation, mapping (function).
Semantic methods in FOL.
Introduction to the thoery of formal proof calculi
Resolution method in propositional logic
General resolution in FOL; Robinson's unification algorithm
Natural deduction in propositional logic
Natural deduction in FOL
Soundness and Completeness of proof calculi
Presentation of the students' solution a given problem.
Theory of relations, types of relations, equivalence and ordering.
Algebraic theories, groups, rings and fields.
Theory of lattices, Formal Conceptual Analysis.
Formalized theories of arithmetic, Gödel's results (completeness and incompleteness)
Hilbert style proof calculi for propositional and predicate logic
Exercises:
Proofs of basic statements of the naive set theory.
Indirect proofs in propositional logic.
Resolution method in propositional logic.
The difference between relation and function, mathematical and empirical examples.
Proofs by semantic tableau in predicate logic.
Set-theoretical semantic proofs in predicate logic.
Traditional Aristoteles logic and the usage of Venn's diagrams.
Proofs of validness using the general resolution method.
Proofs of validness using natural deduction.
Proofs in the theory of relations and functions.
Proofs of basic theorems of arithmetic.
Projects:
Solving a given problem by natural deduction and resolution methods
Conditions for subject completion
Occurrence in study plans
Occurrence in special blocks
Assessment of instruction
Předmět neobsahuje žádné hodnocení.