Informace o předmětu

IA008 Computational Logic

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.: 0/111, pouze zareg. s předností (mateřské obory): 0/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.

IA008 Computational Logic

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: 38/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ě.

IA008 Computational Logic

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: 24/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ě.

IA008 Computational Logic

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: 5/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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Computational Logic

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ě.

IA008 Výpočtová logika

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ě.

IA008 Výpočtová logika

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ě.

• Statistika zápisu (jaro 2025, nejnovější)