Příprava na zkoušku

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

Projděte si úlohy z výrokové i predikátové logiky, které byly řešeny na cvičení nebo ukazovány na přednášce, včetně těch nejjednodušších.

1. Je-li úloha slovní, nejprve ji formalizujte v logice 1. řádu či ve výrokové logice.
2. Jedná-li se o otevřenou úlohu (např. logické hádanky - kdo je poctivec apod.), formulujte hypotézu jako formuli.
3. Snažíte-li se dokázat splnitelnost formulí (neplatnost domněnky), hledejte model.
4. Snažíte-li se dokázat nesplnitelnost formulí (platnost domněnky), převeďte formule a znegovanou hypotézu na klauzule a pomocí rezolučního kalkulu hledejte spor.
5. 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ě, že máte problémy:

• s klauzifikací: zapište formule v TPTP a spusťte na soubor

  eprover --cnf soubor

  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:

#!/bin/bash
(   
    cat <<EOF
set(raw).
set(binary_resolution).
set(print_kept).
set(print_gen).
EOF 
    tptp_to_ladr
) | prover9

• 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.

Výstup z nástroje porovnejte se svými pokusy a srovnejte s teorií. Zkuste znovu danou část provést sami, případně zvolte jednodušší úlohu.