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 TPTP
LeanTAP prover pouzivany v druhe pulce semestru

Cvičení

max 3 omluvene absence
testy behem semestru asi nebudou
nejaka seminarka

Syntax pro solvery:

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

Veci ze cviceni

cv 3: Elitni poctivci a podobna verbez cv 5: Alenka v risi divu

Nase prvni formalizovana domena - John ji Curaky

Linky:

TPTP formalizace

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

leanTAP prover (viz zdroje):

veci bere v NNF (negacni normalovy forme)