taky skuskovy priklad

miso02
Matfyz(ák|ačka) level I
Příspěvky: 16
Registrován: 12. 2. 2006 19:58

taky skuskovy priklad

Příspěvek od miso02 »

Mam problem s jednym skuskovym prikladom a neviem ci som ho dobre vyriesil.
Ak ma niekto vyhrady k mojmu rieseniu tak kludne piste:)

Zadanie:
Dokazte: VyVxB <-> VxVyB

Riesenie:

Najprv pouzijeme vetu o konstantach a vsetky volne premenne v B nahradime konstantami c1..cn, a nech sa tato formula vola A
Podla vety o kostantach je B <-> A.

Zoberme si formulu VyVxA.
Nech n,m su premenne. Podla vety o variantach mozem zamenit viazane premenne v A (v B sme zamenili vsetky premenne konstantami)
Potom VyVxA <-> VnVmA[m,n] (x sme nahradili m a y n) podla vety o variantach
Dalej VnVmA[m,n] <-> (VnVmA[m,n])[x,y] (n nahradime x a m nahradime y)
cize (VnVmA[m,n])[x,y] <-> VxVyA tym je veta dokazana.
Uživatelský avatar
laliebijard
Matfyz(ák|ačka) level III
Příspěvky: 168
Registrován: 8. 6. 2005 10:26
Typ studia: Informatika Mgr.

Příspěvek od laliebijard »

Ja som to robil takto:

Kód: Vybrat vše

|-(Vx)A -> Ax[x]             (axiom specifikacie)
|-(Vy)(Vx)A -> (Vx)Ay[y] (=(Vx)A)      (axiom specifikacie)
|-(Vy)(Vx)A -> A          (zlozenie implikacii)
|-(Vy)(Vx)A -> (Vx)(Vy)A         (dva krat pravidlo zavedenia V)
co myslite?
"posteľ sa rozbieha po koľajniciach z modrého medu"

Breton
Uživatelský avatar
Lada
Donátor
Donátor
Příspěvky: 165
Registrován: 9. 1. 2005 10:17
Typ studia: Informatika Bc.
Bydliště: Slaný / zácpa na Evropské

Příspěvek od Lada »

laliebijard: jojo, napadlo me to samy... a nenapada me co tomu vytknout :twisted:

miso02: nevim jestli jsem to tvoje reseni pochopil spravne, ale neudelas nahodou toto:
VxVy(x<y) prevedes na VyVx(y<x) tedy na to same....?
Hail to you, champion:o)
miso02
Matfyz(ák|ačka) level I
Příspěvky: 16
Registrován: 12. 2. 2006 19:58

Příspěvek od miso02 »

Ano mas pravdu asi to bude tak..
Uživatelský avatar
Dawe
Supermatfyz(ák|ačka)
Příspěvky: 360
Registrován: 12. 10. 2004 12:32
Typ studia: Informatika Mgr.
Bydliště: Doma a nebo na koleji

Příspěvek od Dawe »

laliebijard píše:Ja som to robil takto:

Kód: Vybrat vše

|-(Vx)A -> Ax[x]             (axiom specifikacie)
|-(Vy)(Vx)A -> (Vx)Ay[y] (=(Vx)A)      (axiom specifikacie)
|-(Vy)(Vx)A -> A          (zlozenie implikacii)
|-(Vy)(Vx)A -> (Vx)(Vy)A         (dva krat pravidlo zavedenia V)
co myslite?
Chvíli mi trvalo, než jsem se v tom zorientoval, ale ano, myslím, že je to dobře. Snad jen pro orientaci 1. a 2. formule nejsou ekvivalenty, ale 2 různé formule. Každopádně další rada jak napomoci překonat páteční písemku :-)
Uživatelský avatar
Dan
Matfyz(ák|ačka) level I
Příspěvky: 32
Registrován: 17. 1. 2006 13:32

Příspěvek od Dan »

A nemate niekto navod na nieco taketo:
Dokazte Cons(Cons(T))=Cons(T).
miso02
Matfyz(ák|ačka) level I
Příspěvky: 16
Registrován: 12. 2. 2006 19:58

Příspěvek od miso02 »

Este by som sa chcel spytat na tuto ulohu. Ci je moj postup spravny. Ci som pouzil jednotlive vety korektne..

Zadanie:
Dokazte: ( VxA V VxB ) -> Vx(A v B)

Riesenie? :
Pouzijeme vetu o konstantach a premenne vo formuly nahradime konstantami c1..cn
Potom ak dokazeme upravenu formulu tak plati aj ta povodna.

Dalej pouzijeme vetu o dokaze rozborom pripadov:
Najprv ukazeme VxA |- Vx(A v B) :
|-A -> (A v B) (monotoia disjunkcie)
|-VxA -> Vx(A v B) (distributivita kvantifikatorov)
VxA |- Vx(A v B) (VD)
podobne : VxB |- Vx(A v B)

Teraz podla vety o dokeze rozborom pripadov plati:
( VxA v VxB ) |- Vx(A v B)
|- ( VxA v VxB ) -> Vx(A v B) (VD)

A to by mal byt koniec..
Uživatelský avatar
Dawe
Supermatfyz(ák|ačka)
Příspěvky: 360
Registrován: 12. 10. 2004 12:32
Typ studia: Informatika Mgr.
Bydliště: Doma a nebo na koleji

Příspěvek od Dawe »

To miso02: myslím, že by to mělo být korektní.
miso02
Matfyz(ák|ačka) level I
Příspěvky: 16
Registrován: 12. 2. 2006 19:58

Příspěvek od miso02 »

dik;)
Uživatelský avatar
laliebijard
Matfyz(ák|ačka) level III
Příspěvky: 168
Registrován: 8. 6. 2005 10:26
Typ studia: Informatika Mgr.

Příspěvek od laliebijard »

Dan píše:A nemate niekto navod na nieco taketo:
Dokazte Cons(Cons(T))=Cons(T).
Myslim, ze sa to da robit pomocou def. dokazu
"=>"
musis dokazat, ze pre vsetky A plati Cons(T)|-A => T|-A
Ak A0,...,An=A je dokaz formule A z predp. Cons(T)
potom pre kazde i Ai je bud axiom, to nam nevadi
alebo Ai patri do Cons(T), t.j. T|-Ai, v tom pripade Ai nahradime jej dokazom z T
alebo je odvodena pomocou modus ponens (predpokladame, ze z uz upravenych formuli)
no a mame dokaz formule A z T

a implikacia opacna je este jednoduchsia, lebo
Ai <- T, ale potom aj Ai <- Cons(T), lebo kazda formula z T patri do jej taut. dosledkov.
A mame dokaz Ai v Cons(T).

Teda, ja za spravnost nerucim, neviem, ci to je dobre...
"posteľ sa rozbieha po koľajniciach z modrého medu"

Breton
Uživatelský avatar
Tuetschek
Supermatfyz(ák|ačka)
Příspěvky: 657
Registrován: 15. 6. 2005 13:54
Typ studia: Nestuduji ale učím na MFF
Kontaktovat uživatele:

HILFE!

Příspěvek od Tuetschek »

Cau,
mohl byste se nekdo podivat na tyhle priklady a kdyztak dat nejaky
hint na reseni? Jsem asi uplne neschopnej, ale nemuzu s tim hnout

Kód: Vybrat vše

Která z následujících formulí je dokazatelna? Dokazte syntakticky:
(A->C)->[(B->C)->((A & B)->C)]
(C->(A v C))->(A->C)
Rekl bych ze dokazatelna je prvni a druha ne, ale dokazat to neumim :(.

Kód: Vybrat vše

Zostrojte Skolemovu normálnu formu A_s formule:
(Ey)B <-> ((Vy)B&(Vz)C)
Každá formula obsahuje voľnú iba tú premennú, ktorá je tesne pred ňou
kvantifikovaná.
Pozn.: Neviem, či som dobre opísal zátvorky :(
O Skolemove NF nemam moc poneti - nejaky hint jak se to prevadi?
Plug 'n' Pray.
Uživatelský avatar
Dawe
Supermatfyz(ák|ačka)
Příspěvky: 360
Registrován: 12. 10. 2004 12:32
Typ studia: Informatika Mgr.
Bydliště: Doma a nebo na koleji

Příspěvek od Dawe »

Odpovím jen na první půlku...
Ta druhá není dokazatelná to máš pravdu, a to se nejlíp dokazuje tak, že najdeš protipříklad. Třeba A=1, C=0
Tu druhou jsem dokázal pomocí VD a převedení (A & B)->C pomocí V5 a pravidel na nonC->(A->nonB).

Takže asi takhle:

Kód: Vybrat vše

(A & B)->C 
nonC -> non(A & B) (V5)
nonC -> (nonA v nonB) 
nonC -> (nonnonA -> nonB) (V3)
nonC -> (A -> nonB)

Dál 

(A->C) -> ((B->C) -> (nonC -> (A->nonB)))
(A->C) -> ((nonC->nonB) -> (nonC -> (A->nonB))) (V5)
(A->C) |- ((nonC->nonB) -> (nonC -> (A->nonB))) (VD)
(A->C),(nonC->nonB) |- (nonC -> (A->nonB)) (VD)
(A->C),(nonC->nonB),nonC |- (A->nonB) (VD)
(A->C),(nonC->nonB),nonC,A |- nonB (VD)
pomocí nonC a nonC->nonB přes MP |-nonB

Snad je to dobře.
Uživatelský avatar
laliebijard
Matfyz(ák|ačka) level III
Příspěvky: 168
Registrován: 8. 6. 2005 10:26
Typ studia: Informatika Mgr.

Příspěvek od laliebijard »

K tej Skolemovej variante.

Nuz ja som to pochopil tak, ze zostrojis prenexny tvar formule, oznacme ho A. Potom pre kazdy existencny kvantifikator zavedies novy funkcny symbol a ak A je v tvare (Vx1)...(Vxm)(Ey)B tak ju nahradis (Vx1)...(Vxm)By[f(x1,...xn)], kde n je pocet volnych premennych v B. Postup opakujes, kym sa vo formuli vyskytuje existencny kvantifikator. Dostanes formulu oznacme ju As.

A potom podla lemmy ma platit |- As -> (povodna formula)
"posteľ sa rozbieha po koľajniciach z modrého medu"

Breton
Uživatelský avatar
Tuetschek
Supermatfyz(ák|ačka)
Příspěvky: 657
Registrován: 15. 6. 2005 13:54
Typ studia: Nestuduji ale učím na MFF
Kontaktovat uživatele:

Příspěvek od Tuetschek »

Diky obema :)

Koukam ze jsem poradne nepochopil podstatu dukazu ... to znamena ze kdyz zacnes u ty formule a dojdes k necemu, co uz je zrejmy tak mas dukaz? Ja se pokousel od instance nejakyho axiomu nebo neceho co plati dojit k ty formuli ... neslo :D.

Takze ta Skolemova NF bude vypadat nejak takhle?

Kód: Vybrat vše

(Ey)B <-> ((Vy)B & (Vz) C )

prevod na prenexni formu (nektery mezikroky vynechavam, C_z[q] je substituce q za z v C apod.): 

((Ey) B -> ((Vy)B & (Vz) C)) & (((Vy)B & (Vz) C ) -> (Ey)B)
((Vy)(Vu)(Vz)( B -> (B_y[u] & C)) & ((Ep)(Ew)(Eq)((B_y[w] & C_z[q]) -> B_y[p]))

prenexni forma :

(Vy)(Vu)(Vz)(Ep)(Ew)(Eq) (( B -> (B_y[u] & C))((B_y[w] & C_z[q]) -> B_y[p]))

zavedu nove fcni symboly f, g, h, 
Skolemova NF: 

(Vy)(Vu)(Vz) (( B -> (B_y[u] & C))((B_y[f] & C_z[g]) -> B_y[h]))
A pro operandy tech fcnich symbolu plati nejake omezeni, nebo si muzu proste vzit nejake nove volne promenne?
Plug 'n' Pray.
Uživatelský avatar
laliebijard
Matfyz(ák|ačka) level III
Příspěvky: 168
Registrován: 8. 6. 2005 10:26
Typ studia: Informatika Mgr.

Příspěvek od laliebijard »

Ja by som tam napisal f(x1,...,xn) atd a k tomu, ze n je pocet volnych premennych v danej formuli.
"posteľ sa rozbieha po koľajniciach z modrého medu"

Breton
Odpovědět

Zpět na „2005“