Search
(Jan Jakubův)
Alenka v lese zapomínání: alenka.zip
Ukázka formalizace nádraží ze cvičení: nadrazi.tar.gz
(Jiří Vyskočil)
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ě)