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 |

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

Login | Name | Tuitor | Teacher giving lectures |

DUZ48 | prof. RNDr. Marie Duží, CSc. |

Extent of instruction for forms of study | ||
---|---|---|

Form of study | Way of compl. | Extent |

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

Combined | Credit and Examination | 4+4 |

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.

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.

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

Sochor, A.: Klasická matematická logika. Karolinum Praha, 2001.
Švejdar, V.: Logika, neúplnost a složitost. Academia Praha, 2002.

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.

Subject has no prerequisities.

Subject has no co-requisities.

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

Task name | Type of task | Max. number of points
(act. for subtasks) | Min. number of points |
---|---|---|---|

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

Examination | Examination | 100 | 0 |

Exercises evaluation | Credit | 45 | 0 |

Show history

Academic year | Programme | Field of study | Spec. | Form | Study language | Tut. centre | Year | W | S | Type of duty | |
---|---|---|---|---|---|---|---|---|---|---|---|

2009/2010 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2009/2010 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan | |||

2008/2009 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2008/2009 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan | |||

2007/2008 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2007/2008 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan | |||

2006/2007 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2006/2007 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan | |||

2005/2006 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2005/2006 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan | |||

2004/2005 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2004/2005 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan | |||

2003/2004 | (N2646) Information Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 2 | Compulsory | study plan | |||

2003/2004 | (N2646) Information Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 2 | Compulsory | study plan |

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