Messages

hehe akoze E51, zadabie som zrobil sam ale co tam bolo na pisomke som nemal skoro nic sajnu ale zase skoro nic som sa neucil a cely cas mi trebalo extremne na zachod

ked uz je vsetko zunifikovane, tak tie jednotlive disjunkcie by mali vyzerat rovnako vsetky a faktor je potom ten vzor (jedna disjunkcia)

skripta strana 70, tabulka a pod tym je to napisane

inac ked to nahodou vyvesia na stranke KPI,  to mam hladat hned v tej casti "Informacie pre nasich studentov"  ?

algoritmus na opt. unifikator je takyto priblizne?

- k=0  0  opisat fi1 fi2 fiX    najst Dk { v com sa lisia formuly }

- k=1 { nejaka z Dk / nejaka z Dk + subst. ovplyvni predch. AlfaK },  ficka so substituovanymi vecami,   Dk { zase v com sa lisia }
- az kym sa ficka nerovnaju

ak mam Dk { x, y, z }, je jedno ci substituujem x/y alebo y/x ?

hej, tak nejak, mas jedno co substituujes, ALE v cviceniach aj v skriptach sa vzdy substiovalo
len tak ze  napriklad D{F(a), x} tak to bolo x/F(a) nikdy nie naopak, to tak musi byt ci to len tak si zvolili ?
teda vzdy sme substituovali funkciu za premennu nikdy nie premennu za funkciu

1. jj...toto myslim popripade P(x,a,F(x)) V !P(F(a,x),b)
2. no podla mna ak nebude zadane v ktorej teorii to riesit tak rovnosti (ak tam bude = ) inac by malo byt zadane v ktorej teorii aj s jej axiomami (takto to mam z cviceni), ale to je moj nazor iba

tak nic nerobis, to co sa ti po dosadeni unifikatora bude zhodovat s faktorom vyrucis aj ich doplnky (to su tie co maju pred sebou negaciu) a ostatne nechas, ianc taky priklad ani neni v cviceniahc zeby bol iny predykatovy symbol, inac si pozry ked chces priklad 115 strana 70 skripta, tam je to tak na par riadkov vysvetlene

nic take, nikto nech nad TBIS uz neuvazuje, zatial je tam 28 ludi a tak nech to ostane, bo este jak ma z toho vyrucia ta uz nervy chytim

ale override pouzivas podla mna castejsie ako namespace, a uz mas jedno ci virtual abo jaky

lebo z nasho pohladu, otvorim Visualko dam novy program a namespace tam uz je takze to ani neriesim

vidim, ze si toho este vela nekodil okrem toho zadania
jou ale tesim sa na reakcie na skusku

no ono zadanie som robil v Jave taze tak

a este jednu otazku by som mal? da sa urobit unifikacia ak nema kazdy disjunkt rovnaky predikatovy symbol? (myslim aj jeho negaciu)

edit: pozeram do zosita a tam kde je pouzita ina teoria ako teoria rovnosti, tak je zadane o aku teoriu ide aj s jej axiomami

celkom nechapem tu cast "rovnaky predikatovy symbol" akoze namiesto "P(x,a,F(x)) V P(F(a,x),b)"  tam bude napriklad P(x,a,F(x)) V G(F(a,x),b)

a no ono tam na cviceni nam bolo povedane ze to je v teorii grup, ale ak sa pozries na ten priklad co som postol a v skriptach strana 54 konkretne Zelmerova teoria mnozin, tak tak prva cast toho mojho postnuteho prikladu (po znak |-) je vlastne 1.axioma tejto teorie, tak co ak tym padom myslia v tejto teorii aby sme to riesili ?

tak tie formuly co tam uz mas napisane prepises pomocou unifikatoru, a tie ktore sa budu zhodovat s faktorom, alebo ich doplnky (to akoze ked je pred nimi ! (negacia)) sa budu zhodovat s faktorom, tak tie vyhodis a co ti ostane je rezolventa, a vsetko je spojene pomocou disjunkcie

no ale sak v tom neni ziadna funkcia konkretne v tom priklade co som postol ne ? a to mi malo platit na R2 sa ma vztahovat na predikat ne ??

EDIT: no ale vlastne ked druhu klauzulu uzavries a znegujes tak budes mat funkciu tam takze R3 pouzijes koniec koncov

no toto som napriklad vedel

trochu zvláštne také namespace-i sa používajú viac ako virtual/override

ale override pouzivas podla mna castejsie ako namespace, a uz mas jedno ci virtual abo jaky

lebo z nasho pohladu, otvorim Visualko dam novy program a namespace tam uz je takze to ani neriesim

no ved toto ma zaujima lebo na cviku sme mali priklad ze

|-  x<>y=y<>x  a rovnost tam ostala ale zaroven to bolo v teorii grup a uz si tam pridaval axiomy z teorie grup, lenze hadam nechcu aby som sa uzil vsetky axiomy tych teorii co su v skriptach naspamet, neni povoleny dajaky tahak


EDIT a este v tom priklade co som postol, ktore vsetky by ste pouzili ? R1 a R2 (rovnost) urcite ale ostatne R2(predikat) a R3 ??

ano ja viem presne tento vseobecny postup ale, ako viem aky je to system ci s rovnostou abo jaky ?? ked to nenapise

no fasa a to jak som mal vediet btw ? bars v materialoch take veci tam nesu popisane

no ta do rici, inac to som este nevidel napisane takto, furt sa to zacinalo rovno Console.daco,

viem ze sa opakujem, ale vie dakto toto vypocitat ??

6. Separujte klauzuly pre pouzitie rezolucnej metódy pri odvodení

kto vie kedy sa doplnaju dalsie pary zatvoriek pri unifikacii?

nechapem otazku

www.topjobs.sk

no ale myslim, ze ked si zrobim toten CCIE (abo jak to je) a este aj dajake certifikaty z Javy, asi sa nebudem pri hladany prace zameriavat na Slovensky trh

btw: dneska som mal skusku ale ta v indexe len zapocet mam zapisany, tak nejak mi uniklo ze co dalej s tym

heh inac s tymi bakalarkami popri skuske som sa dneska napriklad pytal Klainovej, ze ci nevie daco o bakalarkach a mi spotila, ze ona uz ma len dve volne (a to este ani neboli zverejnene) a typek co tam sedel v kancli s nou uz iba jednu mal volnu, taze ktovie kolko ich uz je rozobranych, vidim ze bakalarske temy to pomaly jak podpultovy predaj

sak vravi ze co je PO CCNP

ale vlastne v ramci EU nesu hranicne kontroli takze to mam u prdele

ale inac to aj dajaka ina fakulta jak KPI by mohla vypisovat bakalarky ne ?

a piatok dve skusky ta zajtra nemam cas ani ja bars tam sa srat s tym, ked to tam nebude po skuske zo sieti ta fuck off

no ale v prdeli je ze: "Přistoupit by na něj mohla jak Evropská unie" co ma sere o hodne viac teda

ta v kurikulu je k tomu napisane toto: "If there are multiple equal cost paths to this network, there will be multiple successors."

inac ta druha odpoved co je cervenym zaskrtnuta neni dobre