Matematická logika

[Padres]

btw to ten problem dostaneme vyriesit alebo si mozeme nejaky vybrat (ako u dokazani metavety)? Inak tie metavety sa ucite vsetky? Pozeram sak ich tam je po ***** (zehnane) .

[kOsTi]

myslim ze dostanes zadany

[Havran]

na ftp je take pdf ze "vzor" co ma predstavovat asi vzorovu pisomku a

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


a teraz jak to mam riesit ?? bo neni tam uvedene v jakej teorii, ale tie axiomy su jak v Zelmerovej teorii mnozin zo skrip, taze to chcu aby som si pametal vsetky axiomy co su v skriptach

[Padres]

logika je na prvom (starom) FTP,
btw tie problemy nema niekto vypracovane? Resp. niekde na nete nesu vypracovane?

[Dragon]

len presuvam...nechce sa mi stale preklikavat

- lubovolnu metavetu
- dokazat zakon dunsa scotta
- abeceda a jazyk teorie 1.radu
- daka metaveta o dedukcii
- vlastna tvorba jazyka

-mv o nahradení, syntaktická verzia
-dokázať, že axiómy výrokovej logiky sú tautológie
-ľubovoľná MV zo sémantiky PL + dôkaz
-rozšírenie teórie, konzervatívne rozšírenie teórie, ekvivalentnosť teórií
a potom jazyk a príklady... ten istý typ ako vzor...

[buhehe]

to je z minuleho roku? (podla tej tvorby jazyka)....lebo toho roku bude ina skuska...

[Dragon]

jj ja mam zapisane ze bude:
1.formulovat metavetu...asi urcenu cize napr. skolemovu
2.vybrat si metavetu , formulovat a vykonat overenie...lubovolnu
3.riesenie nejakeho problemu...??
4.vysvetlit , definovat...??
5.6.priklady ktore neboli na zapoctovke

cize velky rozdiel tam nie je

[Havran]

no hej, ja osobne problem kladiem bo to nemam sancu sa naucit tam tie vsetky, a v podstate nemam ani sajnu jak ich vyriesit

[buhehe]

kto vie kedy sa doplnaju dalsie pary zatvoriek pri unifikacii?

[Havran]

kto vie kedy sa doplnaju dalsie pary zatvoriek pri unifikacii?

nechapem otazku

[kOsTi]

kto vie kedy sa doplnaju dalsie pary zatvoriek pri unifikacii?

kazdemu funk. symbolu musi zodpovedat jeden par zatvoriek... (nie viac, ani menej)

[Dragon]

okrem tahakov treba tlacit aj nejaky dvojharok s hlavickou ? 

[sri]

hodte sem niekto tahaky, pekne prosiiim
som sa ucil od vikendu a tak som myslel, ze nebudu potrebne   

[Havran]

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

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

[buhehe]

1. uzavries formulu
2. ekviv. problem je taky ze system prvej formuly a negacie druhej je sporny
3. das vsetky formuly na prenexny tvar
4. najdes otvoreny skolemovsky uzaver
5. ked to je system s rovnostou tak musis pridat tie R1-R3
6. kazdu formulu das na konjunktivny normal tvar
7. vypises klauzuly
8. kupis si pivo

[Padres]

no vseobecny postup by mal byt ze:
uzavriet setko ,
znegovat toto co je napravo od |---
previest do skolemovskeho oneho obidve tieto
su tam rovna sa, patri, a ked prevediet do skolemovskeho oneho, ta bude tam aj funkcia, takze napises este R1 (koli rovnasa), R2 (rovnasa), R2(patri), R3(koli funkcii)
tie Rxka odstranit z nich => a <=> a negacie dovnutra
separacia klauzul asi tak ze vyberes tie veci medzi &, indexy u roznych formul rozne, abo jak

tak som tomu aspon ja pochopil opravte ma pls ak sa mylim

[Havran]

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

[buhehe]

no ved ked tam mas = tak je to system s rovnostou

[Padres]

a keby tam nebolo = ale povedzme symboly mnozin alebo take veci? v com sa zmeni postup?

[Havran]

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 ??

[Padres]

Tak podla mna R3 musis pouzit stale ak je nejaka funkcia tam..., a R2 som pocul ze koli tomu symbolu e (patri)...

[Havran]

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

[Padres]

no ale ked spravis otvoreny skolemovsky variant tych formul tam, tak sa tam funkcia vyskytne...

[buhehe]

ako sa odvadza rezolventa? nemate nejaky algoritmus? thx

[Havran]

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