====== 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 - {{:courses:a4m33au:01-uvod.pdf|slidy}}, {{:courses:a4m33au:01-priklady-tptp.zip|příklady}}  |
|  2 |  2.3. | Výroková rezoluce - {{:courses:a4m33au:02-vyrok_rezol.pdf|slidy}} |
|  3 |  9.3. | Rezoluce v logice 1. řádu - {{:courses:a4m33au:03-pred_rezol.pdf|slidy}} |
|  4 |  16.3. | Unifikace, rezoluce s rovností, optimalizace rezoluce {{:courses:a4m33au:04-unifikace-optim-rez.pdf|slidy}}, {{:courses:a4m33au:unifikace.pdf|popis unifikacniho algoritmu}} |
|  5 |  23.3. | ANL smyčka, uspořádaná rezoluce, sémanticky řízená rezoluce (hyperrezoluce, set of support) - {{:courses:a4m33au:05-hyperrez.pdf|slidy}}, {{:courses:a4m33au:priklady-5.zip|priklady}}; {{:courses:a4m33au:priklady-5-cv.zip|}} |
|  6 |  30.3. | Model checking pro timed automata {{:courses:a4m33au:10-model_checking.pdf|slidy}} |
|  7 |  6.4. | Metody použití dokazovačů {{:courses:a4m33au:06-metody-pouziti-atp.pdf|slidy}}, {{:courses:a4m33au:priklady-6.zip|priklady}} |
|  8 |  13.4. | Limity formalních metod {{:courses:a4m33au:07-limity-formalnich-metod.pdf|slidy}} |

Alenka v lese zapomínání: {{:courses:a4m33au:alenka.zip|}}

Ukázka formalizace nádraží ze cvičení: {{:courses:a4m33au:nadrazi.tar.gz|}}

(Jiří Vyskočil)
^ č.t. ^ datum ^ náplň ^
|   9 |  20.4. | Model checking II {{:courses:a4m33au:11-model_checking_ii.pdf|slidy}} |
|  10 |  27.4. | Model checking III {{:courses:a4m33au:12-model_checking_iii.pdf|slidy}} |
|  11 |   4.5. | SAT a DPLL {{:courses:a4m33au:09-dpll.pdf|slidy}} |
|  12 |  11.5. | Nahradni vyuka za Pondeli dle harmonogramu FEL |
|  13 |  18.5. | Hledání modelů v predikátové logice 1. řádu {{:courses:a4m33au:13-model_finding_methods.pdf|slidy}} |
|  14 |  25.5. | Tableaux metody {{:courses:a4m33au:08-tableaux.pdf|slidy}} |

LeanTAP: {{:courses:a4m33au:leantap.txt|}}

MiniSat: {{:courses:a4m33au:minisat_v1.14_linux_static.tar.gz|}} {{:courses:a4m33au:minisat_v1.14_windows.zip|}}

Truth, Lie and Wisdom: {{:courses:a4m33au:truth_lie_and_wisdom.txt|}}
<code>
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)))).
</code>

wolf-cabbage-goat problém v UPPAALu: {{:courses:a4m33au:wolf_cabbage_goat.zip|}}

hra nim v UPPAALu: {{:courses:a4m33au:nim.zip|}}

výtah v UPPAALu: {{:courses:a4m33au:vytah.zip|}}

zadání úlohy v UPPAALu: {{:courses:a4m33au:die_hard.txt|}}

Biphase Mark Protocol v UPPALLu: {{:courses:a4m33au:biphase_mark_protocol.zip|}}

===== Materiály k semestralnímu projektu =====
  * **<fc #FF0000>Zadání [[courses:a4m33au:semestralni_prace|semestrální práce]]</fc>**
  * Pro obecné dotazy k semestrálnímu projektu používejte prosím diskuzní fórum předmětu.
  * {{:courses:a4m33au:order.tptp.zip|axiomatizace lineárního uspořádání}}

===== 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ě: <fc #ff0000>22.5.2017</fc>
        * pro studenty končící na podzim: <fc #ff0000>4.9.2017</fc>

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


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

===== Odkazy =====
  * Odkazy na [[https://cw.felk.cvut.cz/forum|diskusní fórum]] a [[http://cw.felk.cvut.cz/upload/|UploadSystem]]

==== TPTP ====
  * [[http://www.tptp.org|The TPTP Problem Library]] for Automated Theorem Proving (Thousands of 
  * Problems for Theorem Provers)
  * [[http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP|System on TPTP]] - online rozhrani pro dokazovace

==== Dokazovače ====
  * [[http://www.eprover.org/|E prover]]
  * [[http://www.vprover.org/|Vampire]]
  * [[http://www.cs.unm.edu/~mccune/prover9/|Prover 9]], následník dokazovače [[http://www.cs.unm.edu/~mccune/otter/|Otter]]
  * [[http://deepthought.ttu.ee/it/gandalf/|Gandalf]]

==== Hledače modelů ====
  * Paradox
    * [[http://code.haskell.org/folkung/|starší verze 2.3]]
    * [[http://www.cse.chalmers.se/~koen/code/folkung.tar.gz|Novější verze 3]] ze [[http://www.cse.chalmers.se/~koen/|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//.
  * [[http://www.cs.unm.edu/~mccune/prover9/|Mace4]]


===== Různé =====
[[osnova]] (ve výstavbě)