Gurantor department | Department of Computer Science | Credits | 6 |

Subject guarantor | prof. RNDr. Marie Duží, CSc. | Subject version guarantor | prof. RNDr. Marie Duží, CSc. |

Study level | undergraduate or graduate | Requirement | Compulsory |

Year | 1 | Semester | summer |

Study language | Czech | ||

Year of introduction | 1999/2000 | Year of cancellation | 2009/2010 |

Intended for the faculties | FEI | Intended for study types | Bachelor |

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

Login | Name | Tuitor | Teacher giving lectures |

CIH053 | PhDr. Martina Číhalová, Ph.D. | ||

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

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 | 3+2 |

Part-time | Credit and Examination | 3+2 |

The course deals with the fundamentals of logic and formal systems. It covers basic notions and methods of propositional and predicate (1st-order) calculus.

The course deals with fundamental notions of propositional logic and 1st order predicate logic. The student obtains some basic knowledge of formal methods of automatic proving and inference. These methods are used in many disciplines of computer science (formal specification of intuitive knowledge, logical programming, artificial intelligence, etc.) and in many other exact disciplines.

Metakides, G. - Nerode, A.: Principles of Logic and Logic Programming. North-Holland, 1996.
http://www.phil.muni.cz/fil/logika/

http://www.phil.muni.cz/fil/logika/

Verification of study:
Written test from semantic methods of propositional logic - max. 15 grades, min. 5 grades.
Written test from semantic methods of 1st orer predicate logic - max. 15 grades, min. 5 grades.
Conditions for credit:
Obtaining at least 15 grades

Subject has no prerequisities.

Subject has no co-requisities.

Lectures:
Introduction to logic: What is the subject matter of logic? Where and how can logic be helpful for us. Logic as the theory of correct argumentation, logical entailment (consequence).
The language of propositional logic. Definition of truth-value connectives.
The analysis of natural language statements in the language of propositional logic. The semantics of propositional logic: valuation, truth-value functions, tautology, contradiction, satisfaction.
Consequence relation in propositional logic. Semantic methods of justifying arguments in propositional logic.
Complete system of connectives. Normal forms, functional completeness, logical consequences of a set of formulae.
Resolution in propositional logic and its using.
Correct arguments that are not analysable in propositional logic. Language of 1st-order predicate logic, free and bound variables, collisionlessly substituting terms for variables.
Semantics of the 1st-order predicate logic, the notions of interpretation and model. Analysis of natural language expressions in the language of 1st-order predicate logic.
Satisfaction of formulae, formulae true in an interpretation, logically true formulae, contradictions, the consequence relation in the 1st-order predicate logic.
Semantic methods of proving justified arguments. Traditional (Aristotelian) logic.
Deduction in the 1st-order predicate logic, semantic tableau. The set of logically true formulae is not decidable.
Formal systems. Characteristics and features of formal systems. The set of axioms and theorems. The notion of a proof in a formal system. Completeness of 1st-order predicate logic.
Theoretical fundamentals of logic programming. Prenex normal forms, Skolem's clausal forms, Herbrand's procedure - the basic resolution method.
General resolution method and Robinson's unification algorithm.
Exercises:
Examples of arguments formulated in natural language
The analysis of sentences in the language of propositional logic
Negation of sentences
Semantic methods of justifying arguments in propositional logic
Normal forms of formulae in propositional logic
Logical consequences of the set of formulae
Resolution method in propositional logic and its using
The analysis of natural language sentences in the predicate logic
Negation of sentences, equivalent transformations
Interpretation of formulae, models
Semantic methos of justifying arguments in predicate logic
Scolem's clausal forms
Resolution in predicate logic
Proof in a formal system. Gentzen's natural deduction

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. | Zaměření | Form | Study language | Tut. centre | Year | W | S | Type of duty | |
---|---|---|---|---|---|---|---|---|---|---|---|---|

2009/2010 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2008/2009 | (B2646) Information Technology | (1103R021) Computation Mathematics | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2008/2009 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2007/2008 | (B2646) Information Technology | (1103R021) Computation Mathematics | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2007/2008 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2007/2008 | (B2646) Information Technology | (2612R025) Computer Science and Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2007/2008 | (B2646) Information Technology | (2612R025) Computer Science and Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2007/2008 | (B2646) Information Technology | (2612R059) Mobile Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2007/2008 | (B2646) Information Technology | (2612R059) Mobile Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2006/2007 | (B2646) Information Technology | (1103R021) Computation Mathematics | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2006/2007 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2006/2007 | (B2646) Information Technology | (2612R025) Computer Science and Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2006/2007 | (B2646) Information Technology | (2612R025) Computer Science and Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2006/2007 | (B2646) Information Technology | (2612R059) Mobile Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2006/2007 | (B2646) Information Technology | (2612R059) Mobile Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2005/2006 | (B2646) Information Technology | (1103R021) Computation Mathematics | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2005/2006 | (B2646) Information Technology | (2612R025) Computer Science and Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2005/2006 | (B2646) Information Technology | (2612R025) Computer Science and Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2005/2006 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2005/2006 | (B2646) Information Technology | (2612R059) Mobile Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2005/2006 | (B2646) Information Technology | (2612R059) Mobile Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2004/2005 | (B2646) Information Technology | (1103R021) Computation Mathematics | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2004/2005 | (B2646) Information Technology | (2612R025) Computer Science and Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2004/2005 | (B2646) Information Technology | (2612R025) Computer Science and Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2004/2005 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2004/2005 | (B2646) Information Technology | (2612R059) Mobile Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2004/2005 | (B2646) Information Technology | (2612R059) Mobile Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2003/2004 | (B2646) Information Technology | (1103R021) Computation Mathematics | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2003/2004 | (B2646) Information Technology | (2612R025) Computer Science and Technology | P | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2003/2004 | (B2646) Information Technology | (2612R025) Computer Science and Technology | K | Czech | Ostrava | 1 | Compulsory | study plan | ||||

2003/2004 | (B2646) Information Technology | (1103R021) Computation Mathematics | K | Czech | Ostrava | 1 | Compulsory | study plan |

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