IA008 Computational Logic

Faculty of Informatics
Spring 2025
Extent and Intensity
2/2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
In-person direct teaching
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Prerequisites
some familiarity with basic notions from logic like: formula, model, satisfaction, logical equivalence.
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 49/111, only registered with preference (fields directly associated with the programme): 34/111
fields of study / plans the course is directly associated with
there are 33 fields of study the course is directly associated with, display
Course objectives
The course is about algorithmic problems related to logic. The focus is on model checking and satisfiability algorithms for several logics used in the various fields of computer science, for instance in verification or knowledge representation.
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and/or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Ehrenfeucht-Fraise games.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
    recommended literature
  • ENDERTON, Herbert B. A mathematical introduction to logic. 2nd ed. San Diego: Harcourt/Academic press, 2001, xii, 317. ISBN 0122384520. info
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • EBBINGHAUS, Heinz-Dieter, Jörg FLUM and Wolfgang THOMAS. Mathematical logic. Third edition. Cham: Springer, 2021, ix, 304. ISBN 9783030738389. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
The course is taught annually.
The course is taught: every week.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024.

IA008 Computational Logic

Faculty of Informatics
Spring 2024
Extent and Intensity
2/2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Mon 19. 2. to Thu 9. 5. Thu 16:00–17:50 D3
  • Timetable of Seminar Groups:
IA008/01: Tue 12:00–13:50 A318, A. Blumensath
IA008/02: Mon 12:00–13:50 C416, A. Blumensath
IA008/03: Tue 14:00–15:50 C416, A. Blumensath
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 40/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 52 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2023
Extent and Intensity
2/2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Thu 16. 2. to Thu 11. 5. Thu 10:00–11:50 D1
  • Timetable of Seminar Groups:
IA008/01: Tue 14. 2. to Tue 9. 5. Tue 12:00–13:50 C525, A. Blumensath
IA008/02: Tue 14. 2. to Tue 9. 5. Tue 14:00–15:50 C525, A. Blumensath
IA008/03: Wed 15. 2. to Wed 10. 5. Wed 12:00–13:50 C416, A. Blumensath
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 26/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 52 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2022
Extent and Intensity
2/2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Tue 15. 2. to Tue 10. 5. Tue 10:00–11:50 A318
  • Timetable of Seminar Groups:
IA008/01: Fri 18. 2. to Fri 13. 5. Fri 10:00–11:50 C416, A. Blumensath
IA008/02: Thu 17. 2. to Thu 12. 5. Thu 12:00–13:50 C525, A. Blumensath
IA008/03: Thu 17. 2. to Thu 12. 5. Thu 10:00–11:50 C525, A. Blumensath
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 6/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 51 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2020
Extent and Intensity
2/2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Mgr. Jakub Lédl (seminar tutor)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 8:00–9:50 A318
  • Timetable of Seminar Groups:
IA008/01: Mon 14:00–15:50 B410, A. Blumensath
IA008/02: Mon 16:00–17:50 C511, A. Blumensath
IA008/03: Tue 10:00–11:50 C416, A. Blumensath
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 1/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 51 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2019
Extent and Intensity
2/2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Jakub Lédl (seminar tutor)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Fri 10:00–11:50 D2
  • Timetable of Seminar Groups:
IA008/01: Wed 14:00–15:50 B204, A. Blumensath
IA008/02: Wed 12:00–13:50 A320, A. Blumensath
IA008/03: Mon 14:00–15:50 A320, J. Lédl
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 1/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 51 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2018
Extent and Intensity
2/2/0. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Mgr. Tomáš Rudolecký (seminar tutor)
RNDr. Martin Jonáš, Ph.D. (seminar tutor)
Mgr. Ondřej Nečas (assistant)
RNDr. Karel Vaculík, Ph.D. (assistant)
doc. RNDr. Lubomír Popelínský, Ph.D. (alternate examiner)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Fri 10:00–11:50 D2
  • Timetable of Seminar Groups:
IA008/T01: Tue 18. 9. to Thu 13. 12. Tue 12:00–13:50 115, Thu 20. 9. to Thu 13. 12. Thu 12:00–13:50 115, O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Thu 16:00–17:50 A217, A. Blumensath
IA008/02: Tue 12:00–13:50 A318, A. Blumensath
IA008/03: Mon 17. 9. to Mon 10. 12. Mon 8:00–9:50 B410, M. Jonáš
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 19 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Resolution for propositional logic.
  • Resolution for first-order logic.
  • Prolog.
  • Fundamentals of database theory.
  • Tableaux proofs for first-oder logic.
  • Natural deduction.
  • Induction.
  • Modal logic.
  • Many-valued logics.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2017
Extent and Intensity
2/2/0. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Mgr. Tomáš Rudolecký (seminar tutor)
RNDr. Martin Jonáš, Ph.D. (seminar tutor)
Mgr. Ondřej Nečas (assistant)
RNDr. Karel Vaculík, Ph.D. (assistant)
doc. RNDr. Lubomír Popelínský, Ph.D. (alternate examiner)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Fri 8:00–9:50 D3
  • Timetable of Seminar Groups:
IA008/T01: Wed 20. 9. to Fri 22. 12. Wed 15:00–16:35 106, O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Fri 10:00–11:50 C525, A. Blumensath
IA008/02: Thu 12:00–13:50 C525, A. Blumensath
IA008/03: Mon 18:00–19:50 A218, M. Jonáš
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 19 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Learning outcomes
After successfully completing this course students should be familiar with several logics, including propositional logic, first-order logic, and modal logic. They should be familiar with various proof calculi for these logics and be able to use such calculi to test formulae for satisfiability and or validity. In addition, they should have basic knowledge about automatic theorem provers and they way these work.
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Advanced parts from logic programming; Definite clause grammars; Deductive databases;
  • Tableau proofs in different logics. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2016
Extent and Intensity
2/2/0. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Mgr. Tomáš Rudolecký (seminar tutor)
Mgr. Ondřej Nečas (assistant)
RNDr. Karel Vaculík, Ph.D. (assistant)
doc. RNDr. Lubomír Popelínský, Ph.D. (alternate examiner)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Fri 8:00–9:50 D2
  • Timetable of Seminar Groups:
IA008/01: Thu 18:00–19:50 A218, A. Blumensath
IA008/02: Thu 14:00–15:50 B410, A. Blumensath
IA008/03: Thu 18:00–19:50 C511, T. Rudolecký
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 19 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Advanced parts from logic programming; Definite clause grammars; Deductive databases;
  • Tableau proofs in different logics. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2015
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
RNDr. Karel Vaculík, Ph.D. (seminar tutor)
Dr. rer. nat. Achim Blumensath (assistant)
Mgr. Ondřej Nečas (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 8:00–9:50 D1
  • Timetable of Seminar Groups:
IA008/T01: Tue 22. 9. to Tue 22. 12. Tue 9:40–11:15 106, Thu 24. 9. to Tue 22. 12. Thu 16:20–17:55 108, O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Thu 16:00–17:50 B204, K. Vaculík
IA008/02: Thu 18:00–19:50 B204, K. Vaculík
IA008/03: Wed 16:00–17:50 B204, K. Vaculík
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 19 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Advanced parts from logic programming; Definite clause grammars; Deductive databases;
  • Tableau proofs in different logics. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2014
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Eva Mráková, Ph.D. (seminar tutor)
Mgr. Ondřej Nečas (assistant)
Alexandru Popa, Ph.D. (seminar tutor)
Mgr. Jan Marek (assistant)
RNDr. Karel Vaculík, Ph.D. (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Mon 14:00–15:50 D3
  • Timetable of Seminar Groups:
IA008/T01: Mon 15. 9. to Fri 19. 12. Mon 11:20–12:55 Učebna S4 (35a), Fri 19. 9. to Fri 19. 12. Fri 10:15–11:50 Učebna S10 (56), O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Thu 16:00–17:50 A318, A. Popa
IA008/02: Wed 10:00–11:50 C525, A. Popa
IA008/03: Fri 10:00–11:50 B410, E. Mráková
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 18 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Advanced parts from logic programming; Definite clause grammars; Deductive databases;
  • Tableau proofs in different logics. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Autumn 2013
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Eva Mráková, Ph.D. (seminar tutor)
Alexandru Popa, Ph.D. (seminar tutor)
Mgr. Ondřej Nečas (assistant)
Mgr. Juraj Jurčo (assistant)
Mgr. Jan Popelínský (assistant)
RNDr. Karel Vaculík, Ph.D. (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 8:00–9:50 G101
  • Timetable of Seminar Groups:
IA008/01: Thu 12:00–13:50 G124, E. Mráková
IA008/02: Fri 12:00–13:50 B411, E. Mráková
IA008/03: Tue 8:00–9:50 B410, A. Popa
IA008/04: Thu 18:00–19:50 G331, A. Popa
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 18 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Advanced parts from logic programming; Definite clause grammars; Deductive databases;
  • Tableau proofs in different logics. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2013
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Eva Mráková, Ph.D. (seminar tutor)
RNDr. Mgr. Jana Dražanová, Ph.D. (seminar tutor)
Reshma Ramadurai, PhD. (seminar tutor)
Mgr. Ondřej Nečas (assistant)
Mgr. Juraj Jurčo (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 8:00–9:50 D3
  • Timetable of Seminar Groups:
IA008/01: Wed 10:00–11:50 B410, E. Mráková
IA008/02: Thu 12:00–13:50 B411, E. Mráková
IA008/03: Fri 8:00–9:50 B410, J. Dražanová
IA008/04: Thu 14:00–15:50 G123, R. Ramadurai
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 19 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for propositional and predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
  • PRIEST, Graham. An introduction to non-classical logic : from if to is. 2nd ed. Cambridge: Cambridge University Press, 2008, xxxii, 613. ISBN 9780521854337. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2012
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Eva Mráková, Ph.D. (seminar tutor)
RNDr. Mgr. Jana Dražanová, Ph.D. (seminar tutor)
Mgr. Ondřej Nečas (assistant)
Mgr. Peter Nosáľ (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Mon 16:00–17:50 A107
  • Timetable of Seminar Groups:
IA008/01: Tue 10:00–11:50 B204, E. Mráková
IA008/02: Thu 12:00–13:50 B204, E. Mráková
IA008/03: Wed 12:00–13:50 G123, J. Dražanová
IA008/04: Thu 14:00–15:50 G123, J. Dražanová
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 19 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2011
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Mgr. Eva Mráková, Ph.D. (seminar tutor)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Ondřej Nečas (seminar tutor)
Mgr. Marek Trtík, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Tue 10:00–11:50 D1
  • Timetable of Seminar Groups:
IA008/01: Tue 12:00–13:50 B204, E. Mráková
IA008/02: Thu 10:00–11:50 B204, E. Mráková
IA008/03: Wed 16:00–17:50 G124, M. Trtík
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 18 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2010
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
Mgr. Eva Mráková, Ph.D. (seminar tutor)
Mgr. Tomáš Laurinčík (seminar tutor)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Ondřej Nečas (seminar tutor)
Mgr. Marek Trtík, Ph.D. (seminar tutor)
Mgr. Juraj Jurčo (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Tue 10:00–11:50 D1
  • Timetable of Seminar Groups:
IA008/01: Tue 15:00–16:50 D3, E. Mráková
IA008/02: Thu 14:00–15:50 C511, E. Mráková
IA008/03: Fri 12:00–13:50 B410, T. Laurinčík
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 111 student(s).
Current registration and enrolment status: enrolled: 0/111, only registered: 0/111, only registered with preference (fields directly associated with the programme): 0/111
fields of study / plans the course is directly associated with
there are 18 fields of study the course is directly associated with, display
Course objectives
At the end of the course students should be familiar with main research and applications in computational logic; They will be able to use automatic provers for predicate logic and also for its extensions; They will be familiar with, and able to use, methods for inductive inference in those logics;
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Teaching methods
lectures, exercises.
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2009
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
prof. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D. (seminar tutor)
prof. RNDr. Jan Strejček, Ph.D. (seminar tutor)
Mgr. Jan Doleček (assistant)
Mgr. Tomáš Laurinčík (assistant)
Mgr. Eva Mráková, Ph.D. (assistant)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Tue 10:00–11:50 A107
  • Timetable of Seminar Groups:
IA008/01: Wed 12:00–13:50 B204, J. Strejček
IA008/02: Wed 14:00–15:50 B204, J. Strejček
IA008/03: Mon 10:00–11:50 A107, J. Křetínský
IA008/04: Mon 12:00–13:50 B011, J. Křetínský
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 104 student(s).
Current registration and enrolment status: enrolled: 0/104, only registered: 0/104, only registered with preference (fields directly associated with the programme): 0/104
fields of study / plans the course is directly associated with
there are 15 fields of study the course is directly associated with, display
Course objectives
Logic as a computational tool.
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Assessment methods
A midterm written exam and a written final exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2008
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
prof. RNDr. Jan Strejček, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Wed 12:00–13:50 B003
  • Timetable of Seminar Groups:
IA008/01: Thu 14:00–15:50 B410, J. Strejček
IA008/02: Thu 16:00–17:50 B410, J. Strejček
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 253 student(s).
Current registration and enrolment status: enrolled: 0/253, only registered: 0/253, only registered with preference (fields directly associated with the programme): 0/253
fields of study / plans the course is directly associated with
there are 18 fields of study the course is directly associated with, display
Course objectives
Logic as a computational tool.
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Assessment methods (in Czech)
Předmět je ukončen písemnou zkouškou formou testu.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2007
Extent and Intensity
2/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
prof. RNDr. Jan Strejček, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Tue 12:00–13:50 B410
  • Timetable of Seminar Groups:
IA008/01: Wed 14:00–15:50 B410, J. Strejček
IA008/02: Wed 16:00–17:50 B410, J. Strejček
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 253 student(s).
Current registration and enrolment status: enrolled: 0/253, only registered: 0/253, only registered with preference (fields directly associated with the programme): 0/253
fields of study / plans the course is directly associated with
there are 6 fields of study the course is directly associated with, display
Course objectives
Logic as a computational tool.
Syllabus
  • Introduction to propositional and predicate logic.
  • Deduction: Resolution; Logic programming; Prolog, extralogical features, metainterpreters; Definite clause grammars; Deductive databases; Tableau proofs. Theorem proving in modal logic.
  • Induction: Basics of inductive logic programming; Model inference problem; Assumption-based reasoning and learning; Learning frequent patterns.
  • Logic for natural language processing.
  • Knowledge representation and reasoning: Non-classical logic; Knowledge-based systems; Non-monotonic reasoning; Semantic web.
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Assessment methods (in Czech)
Předmět je ukončen písemnou zkouškou formou testu.
Language of instruction
English
Further Comments
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~popel/lectures/complog/
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2006, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2006
Extent and Intensity
2/1. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
RNDr. Jan Blaťák, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Wed 12:00–13:50 A107 and each even Tuesday 10:00–11:50 B410
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 253 student(s).
Current registration and enrolment status: enrolled: 0/253, only registered: 0/253, only registered with preference (fields directly associated with the programme): 0/253
fields of study / plans the course is directly associated with
there are 6 fields of study the course is directly associated with, display
Course objectives
Logic as a computational tool.
Syllabus
  • Essentials of proof theory in propositional and first-order predicate logic.
  • Technical notions: trees, König lemma, formulae analysis, abstract truth-tables, clausal form.
  • Proofs in the propositional logic: system G, soundness, completeness, proof structure, compactness, cut elimination; resolution, refinements of the resolution, Horn clauses, SLD-resolution.
  • Proof in the propositional logic: substitution, system G, compatness, Skolem-Löwenheim theorem, Herbrand theorem; prenex form, Skolemization, unification, resolution and its refinements, Horn clauses, SLD-resolution.
  • Logic programming: SLD-serching, SLD-resolution trees, semantics. Prolog. Metanterpreters.
  • Datalog and deductive databases
  • Inductive logic programming.
  • Modal logic, nonmonotonic inference, many-valued logic, inference with uncertainty
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Assessment methods (in Czech)
Předmět je ukončen písemnou zkouškou formou testu.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2005
Extent and Intensity
2/1. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
RNDr. Jan Blaťák, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Wed 14:00–15:50 B410
  • Timetable of Seminar Groups:
IA008/01: each even Wednesday 16:00–17:50 D1, J. Blaťák
IA008/02: each odd Wednesday 18:00–19:50 B007, J. Blaťák
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is only offered to the students of the study fields the course is directly associated with.

The capacity limit for the course is 253 student(s).
Current registration and enrolment status: enrolled: 0/253, only registered: 0/253
fields of study / plans the course is directly associated with
there are 6 fields of study the course is directly associated with, display
Course objectives
Logic as a computational tool.
Syllabus
  • Essentials of proof theory in propositional and first-order predicate logic.
  • Technical notions: trees, König lemma, formulae analysis, abstract truth-tables, clausal form.
  • Proofs in the propositional logic: system G, soundness, completeness, proof structure, compactness, cut elimination; resolution, refinements of the resolution, Horn clauses, SLD-resolution.
  • Proof in the predicate logic: substitution, system G, compatness, Skolem-Löwenheim theorem, Herbrand theorem; prenex form, Skolemization, unification, resolution and its refinements, Horn clauses, SLD-resolution.
  • Logic programming: SLD-serching, SLD-resolution trees, semantics. Prolog. Metanterpreters.
  • Datalog and deductive databases
  • Inductive logic programming.
  • Modal logic, nonmonotonic inference, many-valued logic, inference with uncertainty
Literature
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NIENHUYS-CHENG, Shan-Hwei and Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Assessment methods (in Czech)
Předmět je ukončen písemnou zkouškou formou testu.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2004, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2004
Extent and Intensity
2/1. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
RNDr. Jan Blaťák, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Wed 10:00–11:50 B410 and each odd Wednesday 18:00–19:50 B204
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is only offered to the students of the study fields the course is directly associated with.

The capacity limit for the course is 253 student(s).
Current registration and enrolment status: enrolled: 0/253, only registered: 0/253
fields of study / plans the course is directly associated with
there are 6 fields of study the course is directly associated with, display
Course objectives (in Czech)
Logika jako nástroj pro výpočet.
Syllabus
  • Essentials of proof theory in propositional and first-order predicate logic.
  • Technical notions: trees, König lemma, formulae analysis, abstract truth-tables, clausal form.
  • Proofs in the propositional logic: system G, soundness, completeness, proof structure, compactness, cut elimination; resolution, refinements of the resolution, Horn clauses, SLD-resolution.
  • Proof in the propositional logic: substitution, system G, compatness, Skolem-Löwenheim theorem, Herbrand theorem; prenex form, Skolemization, unification, resolution and its refinements, Horn clauses, SLD-resolution.
  • Logic programming: SLD-serching, SLD-resolution trees, semantics. Prolog. Metanterpreters.
  • Datalog and deductive databases
  • Inductive logic programming.
  • Modal logic, nonmonotonic inference, many-valued logic, inference with uncertainty
Literature
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
Assessment methods (in Czech)
Předmět je ukončen písemnou zkouškou formou testu.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.

IA008 Computational Logic

Faculty of Informatics
Spring 2003
Extent and Intensity
2/1. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
Teacher(s)
doc. RNDr. Lubomír Popelínský, Ph.D. (lecturer)
Mgr. Miloslav Nepil, Ph.D. (seminar tutor)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: doc. RNDr. Lubomír Popelínský, Ph.D.
Timetable
Tue 12:00–13:50 A107, Thu 9:00–10:50 D2
Prerequisites (in Czech)
! I008 Computational Logic
Course Enrolment Limitations
The course is only offered to the students of the study fields the course is directly associated with.

The capacity limit for the course is 253 student(s).
Current registration and enrolment status: enrolled: 0/253, only registered: 0/253
fields of study / plans the course is directly associated with
there are 6 fields of study the course is directly associated with, display
Course objectives (in Czech)
Logika jako nástroj pro výpočet.
Syllabus
  • Essentials of proof theory in propositional and first-order predicate logic: sequent calculus and resolution.
  • Technical notions: trees, König lemma, formulae analysis, abstract truth-tables, clausal form.
  • Proofs in the propositional logic: system G, soundness, completeness, proof structure, compactness, cut elimination; resolution, refinements of the resolution, Horn clauses, SLD-resolution.
  • Proof in the propositional logic: substitution, system G, compatness, Skolem-Löwenheim theorem, Herbrand theorem; prenex form, Skolemization, unification, resolution and its refinements, Horn clauses, SLD-resolution.
  • Logic programming: SLD-serching, SLD-resolution trees, semantics.
  • Datalog and deductive databases
  • Inductive logic programming.
  • Modal logic, nonmonotonic inference, many-valued logic, inference with uncertainty
Literature
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NERODE, Anil and Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is also listed under the following terms Spring 2004, Spring 2005, Spring 2006, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Spring 2022, Spring 2023, Spring 2024, Spring 2025.
  • Enrolment Statistics (recent)