456-0535/01 – Introduction to Logic (UDL)

Gurantor departmentDepartment of Computer ScienceCredits6
Subject guarantorprof. RNDr. Marie Duží, CSc.Subject version guarantorprof. RNDr. Marie Duží, CSc.
Study levelundergraduate or graduateRequirementCompulsory
Year1Semestersummer
Study languageCzech
Year of introduction1999/2000Year of cancellation2009/2010
Intended for the facultiesFEIIntended for study typesBachelor
Instruction secured by
LoginNameTuitorTeacher 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 studyWay of compl.Extent
Full-time Credit and Examination 3+2
Combined Credit and Examination 3+2

Subject aims expressed by acquired skills and competences

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

Teaching methods

Summary

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.

Compulsory literature:

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

Recommended literature:

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

Way of continuous check of knowledge in the course of semester

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

E-learning

Další požadavky na studenta

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

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

Conditions for subject completion

Combined form (validity from: 1960/1961 Summer semester)
Task nameType of taskMax. 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
Mandatory attendence parzicipation:

Show history

Occurrence in study plans

Academic yearProgrammeField of studySpec.FormStudy language Tut. centreYearWSType 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

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner