Příprava na zkoušku 2011

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):
   1. převeďte formule a znegovanou hypotézu na klauzule,
   2. pomocí rezolučního kalkulu hledejte spor;
   3. 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.
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.

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:

Zapište formule v TPTP a spusťte na soubor

eprover --cnf soubor

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

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.

Jako bonus příklady z minulých písemek:

• pisemka_1.pdf
• pisemka_2.pdf