(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
osnova (ve výstavbě)