Matematická logika

[buhehe]

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

[Havran]

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 ?

[buhehe]

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

[Padres]

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 ?

[Havran]

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

[Havran]

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

[sri]

Ja mam otazku, co je to vlastne ten faktor? Lebo na to nejak neviem zo skript prist 

[Havran]

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

[Havran]

pismoka bola jak sme vsetci ocakavali, priklady na unifikator a separovanie klauzl a teoreticke samozrejme formulovat zadanu metavetu k jednej z nejakej temy overenie, a dalsie dve som nemal sajnu, no tak uvidime pondelok ze co a jak 

[buhehe]

sk. B
1. dokazat postacujuci system shefferovou algebrou
2. dokazat metavetu zo syntaxe VL
3. napisat def struktury
4. napisat metavetu skolema
5. separacia klauzul (btw bola teoria pribuzenstva a bez jej axiom som bol v <>, tak som len dalej pocital bez nich a len som mu tam uviedol ze by som ich mal pridat )
6. unifikacia a urcenie rezolventy

btw: viem ze vyhodnotenie je v pondelok na katedre matiky (tusim b621) ale neviete kedy?

opravene thx to DeNaTuReMaN

[valec]

o 10.00    BN 621

[puq]

matika bol brutus hlavne to 20minutove cakanie, na presvieten otazky ale teoria 0bodov okrem vlastnej metavety, a priklady mam oba dufam ze dobre a tych 20 bodov nahrabem ale skrivanek bol vpohode, ked som daco nevedel alebo nebol som si isty zavolal som ho a povedal mi to, popripade ma naviedol na to

[Alex]

... a ako to bolo s dozorom? dalo sa opisovat? kolki boli?

[puq]

2ja boli ale nas tam bolo kopu ludi lebo aj z ULA pisali prvaci s nami, a opisovat sa aj dalo...ale som neopisoval, lebo som nemal z coho

[DeNaTuReMaN]

sk. B
1. dokazat postacujuci system shefferovou algebrou
2. dokazat metavetu zo syntaxe PL
3. napisat def struktury
4. napisat metavetu skolema
5. separacia klauzul (btw bola teoria pribuzenstva a bez jej axiom som bol v <>, tak som len dalej pocital bez nich a len som mu tam uviedol ze by som ich mal pridat )
6. unifikacia a urcenie rezolventy

btw: viem ze vyhodnotenie je v pondelok na katedre matiky (tusim b621) ale neviete kedy?

Ta 2 otazka bola sytnax VL v B skupine.

[sri]

Uz su vysledky na IS, teda aspon ja mam ....

[buhehe]

jj aj ja mam.....

[elektrikar]

OT : uz niekto niekomu dal na skuske 5 bodov navyse ked mu chybalo ? 

[Dragon]

ta dufam ze mne da skrivanek v pondelok jeden 

[puq]

ja ma  61 D parada prazdniny inac super opravoval z 30 bodov co som mohol maximalne dostat, lebo 3 ulohy som nemal som dostal 30 bodov ))

[valec]

.... tiez mi chyba 5 bodov 

[Padres]

u mna tiez tak... 

[Padres]

co uz, je to snad posledny predmet typu matika-fyzika-ele , tak si ho uzijeme kus viac jak ostatni

[valec]

kto bol na matike, napiste ako...

pridal niekomu nejake body? hovoril nieco o dalsom termine? opravoval pisomky drsne ?

[Padres]

co ja viem nikomu nic nepridal, ni bod , a pisomky opravoval tak... v pohode dalo by sa povedat, nijak extra nedodzubaval, dalsi termin normalne ako su teraz napisane v IS, otazky vraj toho typu co boli aj na riadnom (snad )