Automatické uvažování (AU)

• Stránky předmětu: http://cw.felk.cvut.cz/doku.php/courses/a4m33au/start
• Přednášející: Petr Pudlak
• Cvičící: Petr Pudlak

• Online dokazovace TPTP
• LeanTAP prover pouzivany v druhe pulce semestru

• 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

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

Linky:

• priklad - Buraky
• formalizace prikladu

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)

Obrazek dotazu: