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 | Choice-compulsory |

Year | 1 | Semester | winter |

Study language | Czech | ||

Year of introduction | 2006/2007 | Year of cancellation | 2009/2010 |

Intended for the faculties | FEI | Intended for study types | Follow-up Master |

Instruction secured by | |||
---|---|---|---|

Login | Name | Tuitor | Teacher 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 study | Way of compl. | Extent |

Full-time | Credit and Examination | 4+4 |

Part-time | Credit and Examination | 10+10 |

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.

Lectures

Individual consultations

Tutorials

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).

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

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.

Conditions for credit:
Three written tests, each of which max. 10 grades.
Maximum grades is thus 30.
Minimum to obtain accreditation 15 grades.

Subject has no prerequisities.

Subject has no co-requisities.

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

Task name | Type of task | Max. number of points
(act. for subtasks) | Min. number of points | Max. počet pokusů |
---|---|---|---|---|

Exercises evaluation and Examination | Credit and Examination | 100 (100) | 51 | 3 |

Exercises evaluation | Credit | 45 (30) | 0 | 3 |

Written exam | Written test | 30 | 15 | 3 |

Examination | Examination | 55 (55) | 0 | 3 |

Written examination | Written examination | 55 | 0 | 3 |

Show history

Conditions for subject completion and attendance at the exercises within ISP:

Show history

Academic year | Programme | Branch/spec. | Spec. | Zaměření | Form | Study language | Tut. centre | Year | W | S | Type 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 |

Block name | Academic year | Form of study | Study language | Year | W | S | Type of block | Block owner |
---|

2009/2010 Winter |