| Course Unit Code | 460-4004/01 |
|---|
| Number of ECTS Credits Allocated | 8 ECTS credits |
|---|
| Type of Course Unit * | Optional |
|---|
| Level of Course Unit * | Second Cycle |
|---|
| Year of Study * | |
|---|
| Semester when the Course Unit is delivered | Winter Semester |
|---|
| Mode of Delivery | Face-to-face |
|---|
| Language of Instruction | Czech |
|---|
| Prerequisites and Co-Requisites | Course succeeds to compulsory courses of previous semester |
|---|
| Name of Lecturer(s) | Personal ID | Name |
|---|
| DUZ48 | prof. RNDr. Marie Duží, CSc. |
| 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). |
| Learning Outcomes of the Course Unit |
|---|
| 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. |
| Course Contents |
|---|
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
|
| Recommended or Required Reading |
|---|
| Required Reading: |
|---|
M.Duží: Mathematical logic.
http://www.cs.vsb.cz/duzi/Mat-logika.html
Z. Manna: Mathematical theory of Computer Science. McGraw-Hill, 1974.
|
M.Duží: Matematická logika. Učební texty VŠB Ostrava.
http://www.cs.vsb.cz/duzi/Mat-logika.html
Z. Manna: Matematická teorie programů. McGraw-Hill, 1974, SNTL Praha 1981.
|
| Recommended Reading: |
|---|
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. |
Švejdar, V.: Logika (neúplnost, složitost, nutnost). Academia, Praha 2002.
Sochor, A.: Klasická matematická logika. Karolinum Praha, 2001.
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. |
| Planned learning activities and teaching methods |
|---|
| Lectures, Seminars, Individual consultations, Tutorials |
| Assesment methods and criteria |
|---|
| Tasks are not Defined |