Výroková a predikátová logika, ZS 2026/2027

Obsah cvičení

Odkazy

• Přednáška

Konzultační hodiny

Ideálně se za mnou přijďte hned na konci cvičení.

Jinak sídlím v kanceláři S207. Můžete se zkusit stavit kdykoliv, ale doporučuji předchozí domluvu emailem (obykle není problém se domluvit hned na druhý den).

Podmínky získání zápočtu

Podmínky získání zápočtu odpovídají podmínkám J. Bulína.

V průběhu semestru budou dva zápočtové testy (na 45 minut, psáno na začátku cvičení). První (zhruba v polovině semestru) bude pokrývat část přednášky “Výroková logika”, druhý (ke konci semestru) část přednášky “Predikátová logika”. Za každý z testů lze získat maximálně 100 bodů. Pro každý z testů budete mít nárok na jeden opravný pokus (termín během prvního týdne zkouškového). Žádné další opravné možnosti nebudou. Kromě testů lze získat dodatečných až 50 bodů:

• 40 bodů za projekt na aplikaci SAT solveru
• 10 bodů za aktivitu na cvičeních

K získání zápočtu je potřeba získat alespoň 40 bodů z každého testu a alespoň 140 bodů celkem.

Termíny testů

• Výroková logika: 16. 11. 2026, vzorový test
• Predikátová logika: 4. 1. 2026, vzorový test

Projekt aplikace SAT solveru

Podrobně si přečtěte následující zadání projektu. Dodržujte všechny pokyny v něm obsažené. Vypracovaný projekt musí splňovat popsané požadavky.

Zadání obsahuje očíslovaný seznam problémů, které můžete řešit (název každého projektu je zároveň odkaz na přesné zadání!). Abychom zajistili, že každý student ve skupině bude řešit jiný problém, bude Vám konkrétní projekt přidělen na základě Vašich preferencí.

Je možné řešit i jiný, vlastní, v seznamu neuvedený problém. V tom případě mi co nejdříve pošlete e-mailem podrobnou definici problému (nebo odkaz na ni).

Termíny:

• do 25. 10. 30. 10. vyjádření preferencí (SIS), případně zaslání vlastních návrhů problémů (emailem)
  • Preference zadejte v SISu (modul Studijní mezivýsledky), formou seznamu odděleného čárkami, např. 15,3,21 (od nejvíce preferovaného k nejméně preferovanému; číslo = pořadové číslo problému v rámci toho seznamu v zadání). Pokud budete mít zájem o vlastní návrh problému, napište mi e-mailem zadání, do seznamu pak uveďte mnou přidělené číslo (pokud problém schválím).
• projekt vám bude přidělen nedlouho poté
• do 15. 11. zadejte odkaz na repozitář svého projektu (SIS, modul Studijní mezivýsledky, pole “Odkaz na repozitář projektu”)
• do 30. 11. 5. 12. musí repozitář obsahovat dokončený projekt, včetně rozumné dokumentace (jak to spustit, formát vstupu, jak kódujete problém,… viz zadání). Z historie commitů musí být jasně patrný průběh vývoje; jeden commit (či několik málo) přidávající celé řešení najednou není akceptovatelný.
  • Budete-li mít projekt hotový před termínem, můžete mi e-mailem dát vědět. Není nutné s kontrolou čekat až do 5. 12.
• v první polovině prosince buďte připraveni mi svůj projekt předvést, budete-li k tomu vyzváni

Příklady na cvičení