====== Automatické uvažování (AU) ======

  * Stránky předmětu: http://cw.felk.cvut.cz/doku.php/courses/a4m33au/start
  * Přednášející: Jiří Vyskočil, Jan Jakubů (bývalo Petr Pudlak)
  * Cvičící: Jiří Vyskočil, Jan Jakubů (bývalo Petr Pudlak)

===== Zdroje =====
  * Online dokazovace [[http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP|TPTP]]
  * [[http://ai.ms.mff.cuni.cz/~vyskocil/tableux/leantap.pl|LeanTAP prover pouzivany v druhe pulce semestru]]

===== Cvičení =====
  * max 3 omluvene absence
  * testy behem semestru asi nebudou
  * nejaka seminarka


Syntax pro solvery: 
<code>
fof(nazev,axiom/conjecture, (...telo vyrazu...)).
![x](..)  vsechna x
?[x](..)  existuje x
~         not
|,&       or,and
=>,<=>,<~> implikace,ekvivalence,xor
</code>

====Veci ze cviceni====
[[http://oi-wiki.cz/doku.php/courses/a4m33au-cv3|cv 3: Elitni poctivci a podobna verbez]]
[[http://oi-wiki.cz/doku.php/courses/a4m33au-cv5|cv 5: Alenka v risi divu]]

====Nase prvni formalizovana domena - John ji Curaky ====
Linky: 
  *  [[http://ai.ms.mff.cuni.cz/~vyskocil/tableaux/priklad.pdf|priklad - Buraky]]
  *  [[http://ai.ms.mff.cuni.cz/~vyskocil/tableaux/priklad-formalizace.pdf|formalizace prikladu]]


TPTP formalizace

<code>
fof(1,axiom,
    ( ! [X] : (jidlo(X) => chutna(john,X)))).

fof(2,axiom,
    ( jidlo(jablka) & jidlo(kure))).

fof(3,axiom,
    ( nazivu(bill))).

fof(4,axiom,
    ( ![X,Y]: (nazivu(X) => nezabilo(X,Y)))).

fof(5,axiom,
    ( jist(bill,buraky))).

fof(6,axiom,
    ( ! [X]: (jist(bill,X) => jist(sue,X)))).

fof(7,axiom,
    ( ![X,Y]: ((jist(X,Y) & nezabilo(X,Y)) => jidlo(Y) )) ).

fof(dotaz,conjecture,
    (chutna(john,buraky))).
</code>


leanTAP prover (viz zdroje):

veci bere v NNF (negacni normalovy forme)

<code>
pastebin dUknridC
</code>

Obrazek dotazu: 

{{au-buraky-leantap-proof.png?1000}}

===== Zkouška =====
[[AU_ZK_26_5_11| Zkouska 26.5.2011]]

[[AU_ZK_23_6_11| Zkouska 23.6.2011]]

[[AU_ZK_26_6_12| Zkouska 26.6.2012]]

[[AU_ZK_27_5_14| Zkouska 27.5.2014]]

[[AU_ZK_03_6_15| Zkouska 3.6.2015]]

[[AU_ZK_26_5_16| Zkouška 26.5.2016]]

[[AU_ZK_16_6_16| Zkouška 16.6.2016]]

[[AU_ZK_13_6_17| Zkouška 13.6.2017]]


===== Příklady ze zkoušky =====

**Převodovka**

Zkoušel jsem v UPPAALU, ale jsou tam deadlock(y) takže je to spíš jen tak pro zajímavost :)
{{:courses:the_prevodovka.zip|}}

**Myška**

VerzeA: {{:courses:mymousea.zip|}}

VerzeB: {{:courses:mymouse2.zip|}}

===== Semestralka =====
2011: [[http://cw.felk.cvut.cz/doku.php/courses/a4m33au/semestralni_prace|Vlakove nadrazi]]

[[courses/a4m33au/semestralka_vlakove_nadrazi|Semestrálka - Vlakové nádraží]]

~~DISCUSSION~~