Warning
This page is located in archive.

a4m33au -- Automatické uvažování

Materiály z přednášek

Automatické dokazování

(Jan Jakubův)

č.t. datum náplň
1 23.2. úvod - slidy, příklady
2 2.3. Výroková rezoluce - slidy
3 9.3. Rezoluce v logice 1. řádu - slidy
4 16.3. Unifikace, rezoluce s rovností, optimalizace rezoluce slidy, popis unifikacniho algoritmu
5 23.3. ANL smyčka, uspořádaná rezoluce, sémanticky řízená rezoluce (hyperrezoluce, set of support) - slidy, priklady; priklady-5-cv.zip
6 30.3. Model checking pro timed automata slidy
7 6.4. Metody použití dokazovačů slidy, priklady
8 13.4. Limity formalních metod slidy

Alenka v lese zapomínání: alenka.zip

Ukázka formalizace nádraží ze cvičení: nadrazi.tar.gz

(Jiří Vyskočil)

č.t. datum náplň
9 20.4. Model checking II slidy
10 27.4. Model checking III slidy
11 4.5. SAT a DPLL slidy
12 11.5. Nahradni vyuka za Pondeli dle harmonogramu FEL
13 18.5. Hledání modelů v predikátové logice 1. řádu slidy
14 25.5. Tableaux metody slidy

LeanTAP: leantap.txt

MiniSat: minisat_v1.14_linux_static.tar.gz minisat_v1.14_windows.zip

Truth, Lie and Wisdom: truth_lie_and_wisdom.txt

fof(1,axiom,(! [X,Y,Z] : ((l(X) & m(Y) & r(Z)) => ((X!=Y) & (X!=Z) & (Z!=Y))) )).
fof(2,axiom,(l(truth) | l(lie) | l(wisdom))).
fof(3,axiom,(m(truth) | m(lie) | m(wisdom))).
fof(4,axiom,(r(truth) | r(lie) | r(wisdom))).
fof(5,axiom,(! [X,Y] : ((l(X) & l(Y)) => (X=Y)) )).
fof(6,axiom,(! [X,Y] : ((m(X) & m(Y)) => (X=Y)) )).
fof(7,axiom,(! [X,Y] : ((r(X) & r(Y)) => (X=Y)) )).
fof(11,axiom,( l(truth) => m(truth) )).
fof(12,axiom,( l(lie) => (~ m(truth)) )).
fof(13,axiom,( l(wisdom) => (m(truth) | (~ m(truth))) )).
fof(21,axiom,( m(truth) => m(wisdom) )).
fof(22,axiom,( m(lie) => (~ m(wisdom)) )).
fof(23,axiom,( m(wisdom) => (m(wisdom) | (~ m(wisdom))) )).
fof(31,axiom,( r(truth) => m(lie) )).
fof(32,axiom,( r(lie) =>  (~ m(lie)) )).
fof(33,axiom,( r(wisdom) => (m(lie) | (~ m(lie))) )).

fof(c,conjecture,(? [X,Y,Z] : (l(X) & m(Y) & r(Z)))).

wolf-cabbage-goat problém v UPPAALu: wolf_cabbage_goat.zip

hra nim v UPPAALu: nim.zip

výtah v UPPAALu: vytah.zip

zadání úlohy v UPPAALu: die_hard.txt

Biphase Mark Protocol v UPPALLu: biphase_mark_protocol.zip

Materiály k semestralnímu projektu

Zápočet

  • Zápočet bude udělen za úspěšné odevzdání semstrálního projektu.
  • Semestrální projekt se bude odevzdávat přes odevzdávací systém.
  • Termín odevzdání semestrálního projektu:
    • pro studenty končící v létě: 22.5.2017
    • pro studenty končící na podzim: 4.9.2017

Zkouška

  • Na výslednou známku ze zkoušky se 50% podílí hodnocení semestrálního projektu a 50% vlastní zkouška. Semestrální práce je hodnocena body 0-5, což odpovídá známkám F-A.
  • Vlastní zkouška bude obsahovat písemnou a ústní část.
  • Obsahem zkoušky bude látka probíraná jak na přednášce, tak ve cvičeních.
  • V případě dobrého výsledku u písemné části a dobrého hodnocení semestrálního projektu bude od ústní části zkoušky upuštěno.

Odkazy

TPTP

Dokazovače

Hledače modelů

Různé

osnova (ve výstavbě)

courses/a4m33au/start.txt · Last modified: 2017/05/03 17:31 by vyskoji1