IA008 Computational Logic

Fakulta informatiky
jaro 2025
Rozsah
2/2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučováno kontaktně
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Předpoklady
some familiarity with basic notions from logic like: formula, model, satisfaction, logical equivalence.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 47/111, pouze zareg. s předností (mateřské obory): 33/111
Mateřské obory/plány
předmět má 33 mateřských oborů, zobrazit
Cíle předmětu
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.
Výstupy z učení
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.
Osnova
  • 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.
Literatura
    doporučená literatura
  • ENDERTON, Herbert B. A mathematical introduction to logic. 2nd ed. San Diego: Harcourt/Academic press, 2001, xii, 317. ISBN 0122384520. info
  • NERODE, Anil a Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
  • EBBINGHAUS, Heinz-Dieter, Jörg FLUM a Wolfgang THOMAS. Mathematical logic. Third edition. Cham: Springer, 2021, ix, 304. ISBN 9783030738389. info
Výukové metody
lectures, exercises.
Metody hodnocení
A final written exam.
Vyučovací jazyk
Angličtina
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024.

IA008 Computational Logic

Fakulta informatiky
jaro 2024
Rozsah
2/2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 19. 2. až Čt 9. 5. Čt 16:00–17:50 D3
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Út 12:00–13:50 A318, A. Blumensath
IA008/02: Po 12:00–13:50 C416, A. Blumensath
IA008/03: Út 14:00–15:50 C416, A. Blumensath
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 40/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 52 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2023
Rozsah
2/2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 16. 2. až Čt 11. 5. Čt 10:00–11:50 D1
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Út 14. 2. až Út 9. 5. Út 12:00–13:50 C525, A. Blumensath
IA008/02: Út 14. 2. až Út 9. 5. Út 14:00–15:50 C525, A. Blumensath
IA008/03: St 15. 2. až St 10. 5. St 12:00–13:50 C416, A. Blumensath
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 26/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 52 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2022
Rozsah
2/2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 15. 2. až Út 10. 5. Út 10:00–11:50 A318
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Pá 18. 2. až Pá 13. 5. Pá 10:00–11:50 C416, A. Blumensath
IA008/02: Čt 17. 2. až Čt 12. 5. Čt 12:00–13:50 C525, A. Blumensath
IA008/03: Čt 17. 2. až Čt 12. 5. Čt 10:00–11:50 C525, A. Blumensath
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 6/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 51 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2020
Rozsah
2/2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Mgr. Jakub Lédl (cvičící)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 8:00–9:50 A318
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Po 14:00–15:50 B410, A. Blumensath
IA008/02: Po 16:00–17:50 C511, A. Blumensath
IA008/03: Út 10:00–11:50 C416, A. Blumensath
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 1/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 51 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2019
Rozsah
2/2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Jakub Lédl (cvičící)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Pá 10:00–11:50 D2
  • Rozvrh seminárních/paralelních skupin:
IA008/01: St 14:00–15:50 B204, A. Blumensath
IA008/02: St 12:00–13:50 A320, A. Blumensath
IA008/03: Po 14:00–15:50 A320, J. Lédl
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 1/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 51 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2018
Rozsah
2/2/0. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Mgr. Tomáš Rudolecký (cvičící)
RNDr. Martin Jonáš, Ph.D. (cvičící)
Mgr. Ondřej Nečas (pomocník)
RNDr. Karel Vaculík, Ph.D. (pomocník)
doc. RNDr. Lubomír Popelínský, Ph.D. (náhr. zkoušející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Pá 10:00–11:50 D2
  • Rozvrh seminárních/paralelních skupin:
IA008/T01: Út 18. 9. až Čt 13. 12. Út 12:00–13:50 115, Čt 20. 9. až Čt 13. 12. Čt 12:00–13:50 115, O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Čt 16:00–17:50 A217, A. Blumensath
IA008/02: Út 12:00–13:50 A318, A. Blumensath
IA008/03: Po 17. 9. až Po 10. 12. Po 8:00–9:50 B410, M. Jonáš
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2017
Rozsah
2/2/0. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Mgr. Tomáš Rudolecký (cvičící)
RNDr. Martin Jonáš, Ph.D. (cvičící)
Mgr. Ondřej Nečas (pomocník)
RNDr. Karel Vaculík, Ph.D. (pomocník)
doc. RNDr. Lubomír Popelínský, Ph.D. (náhr. zkoušející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Pá 8:00–9:50 D3
  • Rozvrh seminárních/paralelních skupin:
IA008/T01: St 20. 9. až Pá 22. 12. St 15:00–16:35 106, O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Pá 10:00–11:50 C525, A. Blumensath
IA008/02: Čt 12:00–13:50 C525, A. Blumensath
IA008/03: Po 18:00–19:50 A218, M. Jonáš
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Výstupy z učení
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.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2016
Rozsah
2/2/0. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Mgr. Tomáš Rudolecký (cvičící)
Mgr. Ondřej Nečas (pomocník)
RNDr. Karel Vaculík, Ph.D. (pomocník)
doc. RNDr. Lubomír Popelínský, Ph.D. (náhr. zkoušející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Pá 8:00–9:50 D2
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Čt 18:00–19:50 A218, A. Blumensath
IA008/02: Čt 14:00–15:50 B410, A. Blumensath
IA008/03: Čt 18:00–19:50 C511, T. Rudolecký
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2015
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
RNDr. Karel Vaculík, Ph.D. (cvičící)
Dr. rer. nat. Achim Blumensath (pomocník)
Mgr. Ondřej Nečas (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 8:00–9:50 D1
  • Rozvrh seminárních/paralelních skupin:
IA008/T01: Út 22. 9. až Út 22. 12. Út 9:40–11:15 106, Čt 24. 9. až Út 22. 12. Čt 16:20–17:55 108, O. Nečas, Nepřihlašuje se. Určeno pro studenty se zdravotním postižením.
IA008/01: Čt 16:00–17:50 B204, K. Vaculík
IA008/02: Čt 18:00–19:50 B204, K. Vaculík
IA008/03: St 16:00–17:50 B204, K. Vaculík
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2014
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Eva Mráková, Ph.D. (cvičící)
Mgr. Ondřej Nečas (pomocník)
Alexandru Popa, Ph.D. (cvičící)
Mgr. Jan Marek (pomocník)
RNDr. Karel Vaculík, Ph.D. (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 14:00–15:50 D3
  • Rozvrh seminárních/paralelních skupin:
IA008/T01: Po 15. 9. až Pá 19. 12. Po 11:20–12:55 Učebna S4 (35a), Pá 19. 9. až Pá 19. 12. Pá 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: Čt 16:00–17:50 A318, A. Popa
IA008/02: St 10:00–11:50 C525, A. Popa
IA008/03: Pá 10:00–11:50 B410, E. Mráková
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
podzim 2013
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Eva Mráková, Ph.D. (cvičící)
Alexandru Popa, Ph.D. (cvičící)
Mgr. Ondřej Nečas (pomocník)
Mgr. Juraj Jurčo (pomocník)
Mgr. Jan Popelínský (pomocník)
RNDr. Karel Vaculík, Ph.D. (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 8:00–9:50 G101
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Čt 12:00–13:50 G124, E. Mráková
IA008/02: Pá 12:00–13:50 B411, E. Mráková
IA008/03: Út 8:00–9:50 B410, A. Popa
IA008/04: Čt 18:00–19:50 G331, A. Popa
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2013
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Eva Mráková, Ph.D. (cvičící)
RNDr. Mgr. Jana Dražanová, Ph.D. (cvičící)
Reshma Ramadurai, PhD. (cvičící)
Mgr. Ondřej Nečas (pomocník)
Mgr. Juraj Jurčo (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 8:00–9:50 D3
  • Rozvrh seminárních/paralelních skupin:
IA008/01: St 10:00–11:50 B410, E. Mráková
IA008/02: Čt 12:00–13:50 B411, E. Mráková
IA008/03: Pá 8:00–9:50 B410, J. Dražanová
IA008/04: Čt 14:00–15:50 G123, R. Ramadurai
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro výrokovou a predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a 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
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2012
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Eva Mráková, Ph.D. (cvičící)
RNDr. Mgr. Jana Dražanová, Ph.D. (cvičící)
Mgr. Ondřej Nečas (pomocník)
Mgr. Peter Nosáľ (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 16:00–17:50 A107
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Út 10:00–11:50 B204, E. Mráková
IA008/02: Čt 12:00–13:50 B204, E. Mráková
IA008/03: St 12:00–13:50 G123, J. Dražanová
IA008/04: Čt 14:00–15:50 G123, J. Dražanová
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2011
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Mgr. Eva Mráková, Ph.D. (cvičící)
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Ondřej Nečas (cvičící)
Mgr. Marek Trtík, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
Út 10:00–11:50 D1
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Út 12:00–13:50 B204, E. Mráková
IA008/02: Čt 10:00–11:50 B204, E. Mráková
IA008/03: St 16:00–17:50 G124, M. Trtík
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2010
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
Mgr. Eva Mráková, Ph.D. (cvičící)
Mgr. Tomáš Laurinčík (cvičící)
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Ondřej Nečas (cvičící)
Mgr. Marek Trtík, Ph.D. (cvičící)
Mgr. Juraj Jurčo (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
Út 10:00–11:50 D1
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Út 15:00–16:50 D3, E. Mráková
IA008/02: Čt 14:00–15:50 C511, E. Mráková
IA008/03: Pá 12:00–13:50 B410, T. Laurinčík
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 111 stud.
Momentální stav registrace a zápisu: zapsáno: 0/111, pouze zareg.: 0/111, pouze zareg. s předností (mateřské obory): 0/111
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Na konci tohoto kurzu bude student seznámen s hlavními proudy ve výpočtové logice; Bude umět využívat automatických důkazových technik pro predikátovou logiku a její rozšíření; Bude umět pracovat s metodami induktivního odvozování v těchto logikách;
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Výukové metody
přednáška, cvičení
Metody hodnocení
Semestrální písemná zkouška a závěrečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2009
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
prof. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D. (cvičící)
prof. RNDr. Jan Strejček, Ph.D. (cvičící)
Mgr. Jan Doleček (pomocník)
Mgr. Tomáš Laurinčík (pomocník)
Mgr. Eva Mráková, Ph.D. (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
Út 10:00–11:50 A107
  • Rozvrh seminárních/paralelních skupin:
IA008/01: St 12:00–13:50 B204, J. Strejček
IA008/02: St 14:00–15:50 B204, J. Strejček
IA008/03: Po 10:00–11:50 A107, J. Křetínský
IA008/04: Po 12:00–13:50 B011, J. Křetínský
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 104 stud.
Momentální stav registrace a zápisu: zapsáno: 0/104, pouze zareg.: 0/104, pouze zareg. s předností (mateřské obory): 0/104
Mateřské obory/plány
předmět má 15 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Metody hodnocení
Semestrální písemná zkouška a závěřečná písemná zkouška.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2008
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
prof. RNDr. Jan Strejček, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
St 12:00–13:50 B003
  • Rozvrh seminárních/paralelních skupin:
IA008/01: Čt 14:00–15:50 B410, J. Strejček
IA008/02: Čt 16:00–17:50 B410, J. Strejček
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253, pouze zareg. s předností (mateřské obory): 0/253
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Metody hodnocení
Předmět je ukončen písemnou zkouškou formou testu.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2007
Rozsah
2/2. 4 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
prof. RNDr. Jan Strejček, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
Út 12:00–13:50 B410
  • Rozvrh seminárních/paralelních skupin:
IA008/01: St 14:00–15:50 B410, J. Strejček
IA008/02: St 16:00–17:50 B410, J. Strejček
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253, pouze zareg. s předností (mateřské obory): 0/253
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • 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.
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Metody hodnocení
Předmět je ukončen písemnou zkouškou formou testu.
Vyučovací jazyk
Angličtina
Informace učitele
http://www.fi.muni.cz/~popel/lectures/complog/
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2006
Rozsah
2/1. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
RNDr. Jan Blaťák, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
St 12:00–13:50 A107 a každé sudé úterý 10:00–11:50 B410
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253, pouze zareg. s předností (mateřské obory): 0/253
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • Základy teorie důkazů v predikátové logice a logice prvního řádu: stromy,
  • Důkazy ve výrokové a predikátové logice: kompaktnost, odstranění řezu. Rezoluce a její zjemnění. Tablové důkazy. Substituce, kompaktnost, Skolemova-Löwenheimova věta, Herbrandova věta; prenexová forma, skolemizace, unifikacece. Hornovy klauzule, SLD-rezoluce.
  • Logické programování a jazyk Prolog. Metainterprety.
  • Datalog a deduktivní databáze
  • Induktivní logické programování.
  • Modální logiky, nemonotónní inference, vícehodnotové logiky, inference s neurčitostí.
  • Logika a zpracování přirozeného jazyka
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Metody hodnocení
Předmět je ukončen písemnou zkouškou formou testu.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Computational Logic

Fakulta informatiky
jaro 2005
Rozsah
2/1. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
RNDr. Jan Blaťák, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
St 14:00–15:50 B410
  • Rozvrh seminárních/paralelních skupin:
IA008/01: každou sudou středu 16:00–17:50 D1, J. Blaťák
IA008/02: každou lichou středu 18:00–19:50 B007, J. Blaťák
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je určen pouze studentům mateřských oborů.

Předmět si smí zapsat nejvýše 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • Základy teorie důkazů v predikátové logice a logice prvního řádu: stromy,
  • Důkazy ve výrokové a predikátové logice: kompaktnost, odstranění řezu. Rezoluce a její zjemnění. Tablové důkazy. Substituce, kompaktnost, Skolemova-Löwenheimova věta, Herbrandova věta; prenexová forma, skolemizace, unifikacece. Hornovy klauzule, SLD-rezoluce.
  • Logické programování a jazyk Prolog. Metainterprety.
  • Datalog a deduktivní databáze
  • Induktivní logické programování.
  • Modální logiky, nemonotónní inference, vícehodnotové logiky, inference s neurčitostí.
  • Logika a zpracování přirozeného jazyka
Literatura
  • NERODE, Anil a 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 a Ronald de WOLF. Foundations of inductive logic programming. Berlin: Springer, 1997, xvii, 404. ISBN 3540629270. info
Metody hodnocení
Předmět je ukončen písemnou zkouškou formou testu.
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2004, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Výpočtová logika

Fakulta informatiky
jaro 2004
Rozsah
2/1. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
RNDr. Jan Blaťák, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
St 10:00–11:50 B410 a každou lichou středu 18:00–19:50 B204
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je určen pouze studentům mateřských oborů.

Předmět si smí zapsat nejvýše 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • Základy teorie důkazů v predikátové logice a logice prvního řádu: stromy,
  • Důkazy ve výrokové a predikátové logice: kompaktnost, odstranění řezu. Rezoluce a její zjemnění. Tablové důkazy. Substituce, kompaktnost, Skolemova-Löwenheimova věta, Herbrandova věta; prenexová forma, skolemizace, unifikacece. Hornovy klauzule, SLD-rezoluce.
  • Logické programování a jazyk Prolog. Metainterprety.
  • Datalog a deduktivní databáze
  • Induktivní logické programování.
  • Modální logiky, nemonotónní inference, vícehodnotové logiky, inference s neurčitostí.
  • Logika a zpracování přirozeného jazyka
Literatura
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NERODE, Anil a Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
Metody hodnocení
Předmět je ukončen písemnou zkouškou formou testu.
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.

IA008 Výpočtová logika

Fakulta informatiky
jaro 2003
Rozsah
2/1. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Miloslav Nepil, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
Út 12:00–13:50 A107, Čt 9:00–10:50 D2
Předpoklady
! I008 Výpočtová logika
Omezení zápisu do předmětu
Předmět je určen pouze studentům mateřských oborů.

Předmět si smí zapsat nejvýše 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Logika jako nástroj pro výpočet.
Osnova
  • Základy teorie důkazů v predikátové logice a logice prvního řádu: stromy, Königovo lemma, abstraktní pravdivostní tabulky, klauzulární forma.
  • Důkazy ve výrokové a predikátové logice: kompaktnost, odstranění řezu. Rezoluce a její zjemnění. Tablové důkazy. Substituce, kompaktnost, Skolemova-Löwenheimova věta, Herbrandova věta; prenexová forma, skolemizace, unifikacece. Hornovy klauzule, SLD-rezoluce.
  • Logické programování a jazyk Prolog.
  • Datalog a deduktivní databáze
  • Induktivní logické programování.
  • Modální(temporální) logiky, nemonotónní inference, vícehodnotové logiky, inference s neurčitostí.
  • Logika a zpracování přirozeného jazyka
Literatura
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
  • NERODE, Anil a Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.