a4m33au -- Automatické uvažování

(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

• Zadání semestrální práce
• Pro obecné dotazy k semestrálnímu projektu používejte prosím diskuzní fórum předmětu.
• axiomatizace lineárního uspořádání

• 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

• 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.

• Náměty, jak se připravovat na zkoušku, najdete na stránce příprava na zkoušku.

• Odkazy na diskusní fórum a UploadSystem

• The TPTP Problem Library for Automated Theorem Proving (Thousands of
• Problems for Theorem Provers)
• System on TPTP - online rozhrani pro dokazovace

• E prover
• Vampire
• Prover 9, následník dokazovače Otter
• Gandalf

• Paradox
  • starší verze 2.3
  • Novější verze 3 ze stránek autora - obsahuje zřejmě nějaké další experimentální moduly, takže se projekt nepřeloží celý, ale nám stačí, že lze přeložit binárku paradox.
• Mace4

osnova (ve výstavbě)