Co jsme dělali

7. cvičení (úterý 19. listopadu)

  • Zápočtový test.

6. cvičení (úterý 5. listopadu)

  • Tablo metoda: hledání modelů teorie. Atomická tabla. Věta o dedukci. Věta o kompaktnosti a její aplikace. Množinová reprezentace CNF formulí. Rezoluce, důkaz/zamítnutí rezolucí, rezoluční strom, rezoluční uzávěr.
  • [Příklady 3], 8–9
  • [Příklady 4], 1–5, 7–9
  • Příští týden cvičení odpadá (děkanský den).
  • [domácí úkol č. 3], termín do úterý 26. 11. (na začátku cvičení).
  • První zápočtový test bude v úterý 19.11.

5. cvičení (úterý 29. října)

  • Teorie: důsledky, modely. Algebra výroků (Lindenbaum-Tarski algebra), počet výroků/teorií až na ekvivalenci. Tablo metoda, tablo z teorie, hledání důkazu nebo protipříkladu.
  • [Příklady 3], 5–8
  • Termín odevzdání 2. domácího úkolu je v úterý 5.11.

4. cvičení (úterý 22. října)

  • Ještě k CNF a DNF. SAT: redukce na 3-SAT, kódování problémů do SAT. 2-SAT, implikační graf. Horn-SAT, jednotková propagace. Teorie, důsledky, vlastnosti a sémantika.
  • [Příklady 2], 2, 4, 5, 7, 12
  • [Příklady 3], 1–5
  • [domácí úkol č. 2], termín do úterý 5. 11. (na začátku cvičení). Chcete-li nějaké větší instance grafů pro testování, podívejte se např. sem.

3. cvičení (úterý 15. října)

Řešení domácího úkolu. Ještě k matematice. Univerzálnost logických spojek. Modely. Hledání CNF a DNF reprezentace formulí, pomocí pravdivostní tabulky a pomocí úprav. 2-SAT, implikační graf.

2. cvičení (úterý 8. října)

  • Ještě syntaxe a sémantika výrokové logiky, Booleovské operátory. Definování vlastností v predikátové logice. Grafy, ekvivalence, částečná uspořádání.
  • [Příklady 1], příklady 5,7–8
  • [domácí úkol], termín do pondělí 12:00, vstup pro SAT solver: input.cnf

1. cvičení (úterý 1. října)

  • Program: Úvod. Výroková a predikátová (prvního řádu, vyšších řádů) logika. Syntaxe výrokové logiky (výrazové/vytvořující stromy, prefixový/infixový/postfixový zápis). Sémantika výrokové logiky (Booleovské operátory, pravdivostní tabulka, Vennův diagram). Vyjadřování vlasností pomocí logiky.
  • [1. sada příkladů, příklady 1–6]

Obecné informace

Požadavky na zápočet

V průběhu semestru budeme psát dva zápočtové testy a dostanete několik domácích úkolů. K získání zápočtu je třeba mít alespoň 70% bodů. (Je možné, že bude možné získat bonusové body.) Předběžná data testů:

  • 19. listopadu
  • 7. ledna

Příklady k procvičení

Příklady na cvičení čerpáme z velké části z předchozích semestrů a od jiných vyučujících, zejména cvičení Petra Gregora nebo cvičení Jana Hrice. Pokud chcete více příkladů, zkuste cvičení na konci kapitol v [knize], nebo mi napiště.