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

Obsah cvičení

Odkazy

• Přednáška

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.

Způsob vyjádření preferencí a odevzdání odkazu na repozitář bude včas upřesněn.

Termíny:

• do 25. 10. zadejte vyjádření preferencí (způsob bude upřesněn), případně zaslání vlastních návrhů problémů (emailem)
• projekt vám bude přidělen nedlouho poté
• do 15. 11. zadejte odkaz na repozitář svého projektu (způsob bude upřesněn)
• do 30. 11. musí repozitář obsahovat dokončený projekt, včetně rozumné dokumentace (jak to spustit, jak kódujete problém,…). 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ý.
• 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í