====== Příprava na zkoušku 2011 ======
Náměty na cvičení, která vám pomohou připravit se ke zkoušce.

===== Úlohy z přednášky a cvičení =====
Projděte si úlohy z výrokové i predikátové logiky, které byly řešeny na cvičení nebo ukazovány na [[start#Materiály z přednášek|přednášce]], včetně těch nejjednodušších.
  - Je-li úloha slovní, nejprve ji formalizujte v logice 1. řádu či ve výrokové logice.
  - Jedná-li se o otevřenou úlohu (např. logické hádanky - kdo je poctivec apod.), formulujte hypotézu jako formuli.
  - Snažíte-li se dokázat splnitelnost formulí (neplatnost domněnky), hledejte model.
  - Snažíte-li se dokázat nesplnitelnost formulí (platnost domněnky):
    - převeďte formule a znegovanou hypotézu na klauzule,
    - pomocí rezolučního kalkulu hledejte spor;
    - při provádění důkazu používejte zpětnou a dopřednou subsumpci - jednak procvičíte pojem subsumpce a jednak tím velmi často zjednodušíte důkaz.
  - Jedná-li se o úlohu s hypotézou, v rámci procvičení hypotézu odstraňte a ponechte pouze axiomy; tato množina formulí bude splnitelná; najděte její model.

==== V případě problémů ====
Může pomoci využít pro problematickou část úlohy odpovídající nástroj (viz. níže). Jeho výstup pak porovnat s vlastními pokusy a s teorií. Zkusit pak znovu danou část úlohy provést samostatně.

Při problémech:
=== s klauzifikací ===
Zapište formule v TPTP a spusťte na soubor <code sh>eprover --cnf soubor</code> který provede klauzifikaci.
=== s dokazováním rezolučním kalkulem ===
Následující shell skript převede formule z TPTP na standardním vstupu do jazyka knihovny LADR, nastaví parametry tak, aby dokazovač prováděl neoptimalizovanou binární rezoluci (takže jsou vidět jednotlivé kroky) a spustí Prover9:
<code sh>
#!/bin/bash
(   
    cat <<EOF
set(raw).
set(binary_resolution).
set(print_kept).
set(print_gen).
EOF 
    tptp_to_ladr
) | prover9
</code>
 
=== s hledáním modelů ===
Najděte model pomocí hledače modelů Paradox nebo Mace4, a poté ručně ověřte, že se skutečně jedná o model, tedy že všechny formule jsou ve výsledné interpretaci splněny.

===== Příklady z předešlých písemek =====
Jako bonus příklady z minulých písemek:
  * {{:courses:a4m33au:pisemka_1.pdf|}}
  * {{:courses:a4m33au:pisemka_2.pdf|}}