CourseWare Wiki
Search
Log In
old
courses
a4m33au
priprava_na_zkousku
Warning
This page is located in archive.
Differences
This shows you the differences between two versions of the page.
View differences:
Side by Side
Inline
Go
Link to this comparison view
Go
Go
courses:a4m33au:priprava_na_zkousku [2011/08/20 19:38]
pudlapet
courses:a4m33au:priprava_na_zkousku [2013/10/04 13:02]
Line 1:
Line 1:
-
====== Příprava na zkoušku ======
-
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|}}
courses/a4m33au/priprava_na_zkousku.txt
· Last modified: 2013/10/04 13:02 (external edit)