taky skuskovy priklad
taky skuskovy priklad
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.
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.
- laliebijard
- Matfyz(ák|ačka) level III
- Příspěvky: 168
- Registrován: 8. 6. 2005 10:26
- Typ studia: Informatika Mgr.
- Login do SIS: repij4am
Ja som to robil takto:
co myslite?
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)
"posteľ sa rozbieha po koľajniciach z modrého medu"
Breton
Breton
- 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
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ísemkulaliebijard píše:Ja som to robil takto:
co myslite?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)
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..
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..
- laliebijard
- Matfyz(ák|ačka) level III
- Příspěvky: 168
- Registrován: 8. 6. 2005 10:26
- Typ studia: Informatika Mgr.
- Login do SIS: repij4am
Myslim, ze sa to da robit pomocou def. dokazuDan píše:A nemate niekto navod na nieco taketo:
Dokazte Cons(Cons(T))=Cons(T).
"=>"
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
Breton
- Tuetschek
- Supermatfyz(ák|ačka)
- Příspěvky: 657
- Registrován: 15. 6. 2005 13:54
- Typ studia: Nestuduji ale učím na MFF
- Login do SIS: duseo7af
- Kontaktovat uživatele:
HILFE!
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
Rekl bych ze dokazatelna je prvni a druha ne, ale dokazat to neumim .
O Skolemove NF nemam moc poneti - nejaky hint jak se to prevadi?
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)
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 :(
Plug 'n' Pray.
- 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
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:
Snad je to dobře.
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
- laliebijard
- Matfyz(ák|ačka) level III
- Příspěvky: 168
- Registrován: 8. 6. 2005 10:26
- Typ studia: Informatika Mgr.
- Login do SIS: repij4am
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)
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
Breton
- Tuetschek
- Supermatfyz(ák|ačka)
- Příspěvky: 657
- Registrován: 15. 6. 2005 13:54
- Typ studia: Nestuduji ale učím na MFF
- Login do SIS: duseo7af
- Kontaktovat uživatele:
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 .
Takze ta Skolemova NF bude vypadat nejak takhle?
A pro operandy tech fcnich symbolu plati nejake omezeni, nebo si muzu proste vzit nejake nove volne promenne?
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 .
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]))
Plug 'n' Pray.
- laliebijard
- Matfyz(ák|ačka) level III
- Příspěvky: 168
- Registrován: 8. 6. 2005 10:26
- Typ studia: Informatika Mgr.
- Login do SIS: repij4am