IB101 Úvod do logiky a logického programování

Fakulta informatiky
jaro 2010
Rozsah
2/2. 4 kr. (plus ukončení). Ukončení: zk.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
doc. RNDr. Jan Bouda, Ph.D. (cvičící)
Mgr. Lukáš Másilko (cvičící)
Mgr. Ondřej Nečas (cvičící)
Mgr. Adam Šiška (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
Po 10:00–11:50 D2, Po 10:00–11:50 D1
  • Rozvrh seminárních/paralelních skupin:
IB101/01: Út 18:00–19:50 D3, J. Bouda
IB101/02: St 18:00–19:50 D2, A. Šiška
IB101/03: Čt 10:00–11:50 D3, J. Bouda
Předpoklady
! IA008 Computational Logic
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
Cíle předmětu
Na konci tohoto kurzu budou studenti rozumět principům výrokové a predikátové logiky 1. řádu a důkazovým technikám, především rezoluční metodě. Budou seznámeni se základy logického programování a výpočtové logiky, induktivního odvozování a reprezentace znalostí.
Osnova
  • Kurs je úvodem do výrokového a predikátového počtu, rezoluční metody, logického programování a výpočtové logiky, induktivního odvozování a reprezentace znalostí.
  • Přehled logických kalkulů, syntaxe.
  • Výroková logika, pravdivostní tabulky, axiomy, dokazatelnost.
  • Základy teorie důkazů ve výrokové logice, normální formy, rezoluce.
  • Predikátový počet 1. řádu, predikátové formule, sémantika, axiomy, dokazatelnost.
  • Normální formy predikátové logiky, skolemizace.
  • Základy teorie důkazů v predikátové logice, rezoluce.
  • Úvod do logického programování, SLD-rezoluce. Jazyk Prolog.
  • Základy induktivního odvozování a reprezentace znalostí.
Literatura
  • ŠTĚPÁN, Jan. Klasická logika. 1. vyd. Olomouc: Univerzita Palackého v Olomouci, 2001, 198 s. ISBN 8024402548. info
  • NERODE, Anil a Richard A. SHORE. Logic for applications. New York: Springer-Verlag, 1993, xvii, 365. ISBN 0387941290. info
Výukové metody
Přednášky, cvičení.
Metody hodnocení
Součástí hodnocení je semestrální zkouška. Předmět je ukončen písemnou zkouškou formou testu, není povoleno používat žádné pomocné materiály.
Navazující předměty
Informace učitele
http://www.fi.muni.cz/usr/popelinsky/lectures/bak_logika/
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, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020.