Syntax pro solvery:
fof(nazev,axiom/conjecture, (...telo vyrazu...)).  vsechna x ?[x](..) existuje x ~ not |,& or,and =>,<=>,<~> implikace,ekvivalence,xor
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)
pastebin dUknridC
Obrazek dotazu:
Převodovka
Zkoušel jsem v UPPAALU, ale jsou tam deadlock(y) takže je to spíš jen tak pro zajímavost :) the_prevodovka.zip
Myška
VerzeA: mymousea.zip
VerzeB: mymouse2.zip