Zápočtový příklad - Vyskočil
- Lukas Mach
- Matfyz(ák|ačka) level III
- Příspěvky: 261
- Registrován: 28. 3. 2006 17:08
- Typ studia: Informatika Bc.
- Bydliště: Praha a Kladno
- Kontaktovat uživatele:
Zápočtový příklad - Vyskočil
Nazdar,
blizi se termin zkousek z Logiky a podle vseho hodne lidi resi priklad od Vyskocila. Dostal jsem dokazat dost jednoduchou formuli v systemu pro vyrokovou logiku s odvozovacim pravidlem modus ponens (tj. zatim celkem easy). Schema (jedineho) axiomu je:
i(i(i(i(i(A,B),i(n(C),n(D))),C),E),i(i(E,A),i(D,A)))
Vzhledem k tomu, ze i nekteri ostatni maji ten samy axiom, tak jsem si rekl, ze s tim zacnu otravovat na foru . Po nejakem tom googlovani jsem zjistil, ze jde o Meredithův axiom a ze je to uplne to same jako ty 3 axiomy z prednašky - jsou ekvivalentní. Ty 3 axiomy se z Meredithova axiomu dají odvodit - nejdřív se z něj odvodí Lukasiewiczovy axiomy a z nich se dájí odvodit ty naše 3 schémata axiomů z přednášky. Celý ten příběh je tady:
http://us.metamath.org/mpegif/meredith.html
Klikejte na next vpravo nahoře a budete se posunovat dál v důkazu. Na první stránce je důkaz Meredithova axiomu ze standardních axiomů (opačný směr), což není moc zajímavé. Pak tam ovšem je ten důkaz správným směrem, rozprostřený přes řadu stránek - přesto to ale není žádná tisíciřádková šílenost vygenerovaná počítačem (mimochodem, četl jsem, že bylo dost problematické, než se podařilo přinutit nějaký systém na automatické dokazování formulí, aby tenhle ještě poměrně jednoduchý důkaz dokázal, takže hledat důkaz pomocí Prologu možná není ta správná cesta).
Můj plán je tedy vytahat z výše uvedeného webu důkaz "Meredith -> Lukasiewicz", potom za to plácnout důkaz "Lukasiewicz -> standardní 3 axiomy" a nakonec někde_najít/vymyslet důkaz té jednoduché formule (kterou mám dokázat) ve standardním systému. Nakonec si možná napíšu prográmek v Prologu na ověřování důkazů (což by mělo být zase jednoduchý).
Tak to já jen pro případ, že by ještě někdo další měl ten samý axiom, popřípadě jako info o tom, že ty Vyskočilovy příklady mají hlubší smysl.
blizi se termin zkousek z Logiky a podle vseho hodne lidi resi priklad od Vyskocila. Dostal jsem dokazat dost jednoduchou formuli v systemu pro vyrokovou logiku s odvozovacim pravidlem modus ponens (tj. zatim celkem easy). Schema (jedineho) axiomu je:
i(i(i(i(i(A,B),i(n(C),n(D))),C),E),i(i(E,A),i(D,A)))
Vzhledem k tomu, ze i nekteri ostatni maji ten samy axiom, tak jsem si rekl, ze s tim zacnu otravovat na foru . Po nejakem tom googlovani jsem zjistil, ze jde o Meredithův axiom a ze je to uplne to same jako ty 3 axiomy z prednašky - jsou ekvivalentní. Ty 3 axiomy se z Meredithova axiomu dají odvodit - nejdřív se z něj odvodí Lukasiewiczovy axiomy a z nich se dájí odvodit ty naše 3 schémata axiomů z přednášky. Celý ten příběh je tady:
http://us.metamath.org/mpegif/meredith.html
Klikejte na next vpravo nahoře a budete se posunovat dál v důkazu. Na první stránce je důkaz Meredithova axiomu ze standardních axiomů (opačný směr), což není moc zajímavé. Pak tam ovšem je ten důkaz správným směrem, rozprostřený přes řadu stránek - přesto to ale není žádná tisíciřádková šílenost vygenerovaná počítačem (mimochodem, četl jsem, že bylo dost problematické, než se podařilo přinutit nějaký systém na automatické dokazování formulí, aby tenhle ještě poměrně jednoduchý důkaz dokázal, takže hledat důkaz pomocí Prologu možná není ta správná cesta).
Můj plán je tedy vytahat z výše uvedeného webu důkaz "Meredith -> Lukasiewicz", potom za to plácnout důkaz "Lukasiewicz -> standardní 3 axiomy" a nakonec někde_najít/vymyslet důkaz té jednoduché formule (kterou mám dokázat) ve standardním systému. Nakonec si možná napíšu prográmek v Prologu na ověřování důkazů (což by mělo být zase jednoduchý).
Tak to já jen pro případ, že by ještě někdo další měl ten samý axiom, popřípadě jako info o tom, že ty Vyskočilovy příklady mají hlubší smysl.
For every epsilon, there is delta.
Where is my delta?
Where is my delta?
DIKY
Diky velmi pekne. Si nasa zachrana. Idem googlit opisovat prepisovat .. len aby som sa po dlhom case nejak dostal na tu skusku Inac na prednaske alebo cvikach niekto hovoril ze existuje axiom z ktoreho sa da odvodit cely hilbertov system, a mal som podozrenie ze to bude tento, len .. nic som nevygooglil. A uz vobec nie dokazy. Btw dostal som dokaz, ze ten axiom je rovnako silny ako hilbertov system a jeden mudrejsi clovek mi na to odpisal taky postup ako si ty volil. Az na to ze nevedel ten link ani ziadnu info z neho. Naspat sa to ma robit cez tabulku pravdivostnych hodnot, takze na to by sa mohol asi pouzit prolog. Uz len dufam ze sa nejako prepracujem k zapoctu... Kazdopadne po mojich neuspesnych skusoch v prologu s dokazovanim
There's nothing left to lose.
- Lucas
- Matfyz(ák|ačka) level I
- Příspěvky: 15
- Registrován: 15. 1. 2007 20:34
- Typ studia: Informatika Mgr.
iny druh domacej
Zdravim.
Ja mam tiez tazku hlavu zo zapoctovej ulohy..
A bol by som aj ochotny podporit vasu ochotu pomoct cloveku v nudzi .. =) .. nejakou odmenou.
Moj priklad:
Uvažujte následující formální systém pro výrokovou logiku s jednou binární logickou spojkou d:
schéma axiomu L: (d(P,d(Q,R)),d(d(P,d(R,P)),d(d(S,Q),d(d(P,S),d(P,S)))))
odvozovaci pravidlo N: Pokud platí d(P,d(Q,R)) a P, pak platí R.
Nalezněte sémantiku tohoto systému (významovou interpretaci spojek a proměnných. Z přednášky například znáte sémantiku pro výrokovou logiku k systém axiomů A1,A2,A3 a pravidla MP) a formálně dokažte, že je korektní.
Lebo I have no f. idea...
pliiiis
Ja mam tiez tazku hlavu zo zapoctovej ulohy..
A bol by som aj ochotny podporit vasu ochotu pomoct cloveku v nudzi .. =) .. nejakou odmenou.
Moj priklad:
Uvažujte následující formální systém pro výrokovou logiku s jednou binární logickou spojkou d:
schéma axiomu L: (d(P,d(Q,R)),d(d(P,d(R,P)),d(d(S,Q),d(d(P,S),d(P,S)))))
odvozovaci pravidlo N: Pokud platí d(P,d(Q,R)) a P, pak platí R.
Nalezněte sémantiku tohoto systému (významovou interpretaci spojek a proměnných. Z přednášky například znáte sémantiku pro výrokovou logiku k systém axiomů A1,A2,A3 a pravidla MP) a formálně dokažte, že je korektní.
Lebo I have no f. idea...
pliiiis
Hele mozku, nemáš rád mně a ja zas tebe. Ale tohle musíme udělat a pak tě vyřídim jedním pivem.
Re: iny druh domacej
Ahoj, mam stejny axiom a pravidlo, ale mam dokazat tuto formuli:Lucas píše:Zdravim.
Ja mam tiez tazku hlavu zo zapoctovej ulohy..
A bol by som aj ochotny podporit vasu ochotu pomoct cloveku v nudzi .. =) .. nejakou odmenou.
Moj priklad:
Uvažujte následující formální systém pro výrokovou logiku s jednou binární logickou spojkou d:
schéma axiomu L: (d(P,d(Q,R)),d(d(P,d(R,P)),d(d(S,Q),d(d(P,S),d(P,S)))))
odvozovaci pravidlo N: Pokud platí d(P,d(Q,R)) a P, pak platí R.
Nalezněte sémantiku tohoto systému (významovou interpretaci spojek a proměnných. Z přednášky například znáte sémantiku pro výrokovou logiku k systém axiomů A1,A2,A3 a pravidla MP) a formálně dokažte, že je korektní.
Lebo I have no f. idea...
pliiiis
d(d(d(d(d(a,a),d(a,a)),d(a,a)),d(d(d(a,a),d(a,a)),d(a,a))),d(d(d(d(a,a),d(a,a)),d(a,a)),d(d(d(a,a),d(a,a)),d(a,a))))
zatim jsem si napsal program co udela dokazovaci strom toho axiomu - kdyz ho chces dokazat, vzniknou formule
1 a d(1,d(2,formule)) kde 1 a 2 jsou volne promenne, a z kazde z nich zase generuju 2 nove formule co je dokazuji, a v tom stromu potrebuju najit nejakou mnozinu formuli co ho 'urizne', takovou, ze ty ciselne volne promenne v te mnozine formuli jsou stejne a zaroven vsechny formule z mnoziny unifikuji s nejakou instanci axiomu (aneb unifikuji s axiomem kde velka pismena PQRS jsou volne promenne, pro kazdou formuli jine).
Ted resim jak hledat tu mnozinu ve stromu, asi je nutne vyzkouset vsechno - existuje ostre usporadani na podmnozinach stromu? (edit: asi jo - ocislovat po patrech zleva doprava a z toho pak vybirat podmnoziny podle bin, zapisu cisel: 1 01 10 11 ...)
Mate nejaky napad?
Re: iny druh domacej
Prijde mi ze tohle zadani uz jsem tu nekde videl (neni to to samy jako mel Greg http://forum.matfyz.info/viewtopic.php?t=3259?).keff píše:
Ahoj, mam stejny axiom a pravidlo, ale mam dokazat tuto formuli:
d(d(d(d(d(a,a),d(a,a)),d(a,a)),d(d(d(a,a),d(a,a)),d(a,a))),d(d(d(d(a,a),d(a,a)),d(a,a)),d(d(d(a,a),d(a,a)),d(a,a))))
zatim jsem si napsal program co udela dokazovaci strom toho axiomu - kdyz ho chces dokazat, vzniknou formule
1 a d(1,d(2,formule)) kde 1 a 2 jsou volne promenne, a z kazde z nich zase generuju 2 nove formule co je dokazuji, a v tom stromu potrebuju najit nejakou mnozinu formuli co ho 'urizne', takovou, ze ty ciselne volne promenne v te mnozine formuli jsou stejne a zaroven vsechny formule z mnoziny unifikuji s nejakou instanci axiomu (aneb unifikuji s axiomem kde velka pismena PQRS jsou volne promenne, pro kazdou formuli jine).
Ted resim jak hledat tu mnozinu ve stromu, asi je nutne vyzkouset vsechno - existuje ostre usporadani na podmnozinach stromu? (edit: asi jo - ocislovat po patrech zleva doprava a z toho pak vybirat podmnoziny podle bin, zapisu cisel: 1 01 10 11 ...)
Mate nejaky napad?
Jediny co ti muzu doporucit je zkusit si stahnout treba prover9 - ten by mohl ten dukaz najit http://www.cs.unm.edu/~mccune/prover9/. Hodne stesti.
Re: iny druh domacej
Díky moc za linky, k Proveru už jsem se doklikal včera včera ale už se radši budu učit na zk. a pak snad přijdu jak to do proveru naťukat .jirka_v píše: Prijde mi ze tohle zadani uz jsem tu nekde videl (neni to to samy jako mel Greg http://forum.matfyz.info/viewtopic.php?t=3259?).
Jediny co ti muzu doporucit je zkusit si stahnout treba prover9 - ten by mohl ten dukaz najit http://www.cs.unm.edu/~mccune/prover9/. Hodne stesti.
Re: iny druh domacej
Neni zac. Pro inspiraci jeste prikladam vstupni soubor pro prover9 k dokazani (v7) v Hilbertove systemu.keff píše: Díky moc za linky, k Proveru už jsem se doklikal včera včera ale už se radši budu učit na zk. a pak snad přijdu jak to do proveru naťukat .
Kód: Vybrat vše
formulas(sos).
P(i(x,i(y,x))). %axiom A1
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). % axiom A2
P(i(i(n(y),n(x)),i(x,y))). %axiom A3
-P(i(x,y)) | -P(x) | P(y). % modus ponens
-P(i(i(n(a),a),a)). % v7 (nebo spis jeji negace)
end_of_list.
Re: iny druh domacej
Můžu ještě využít tvé know-how pro vysvětlení techle dvou řádků?jirka_v píše:Kód: Vybrat vše
-P(i(x,y)) | -P(x) | P(y). % modus ponens -P(i(i(n(a),a),a)). % v7 (nebo spis jeji negace) end_of_list.
a) jak Prover pozná že MP může použít a v7 má dokázat, když mají ty dva řádky stejopu syntax?
b) řádek s MP znamená 'y platí, nebo x neplatí, nebo implikace x->y je nepravdivá'?
Re: iny druh domacej
Hmm, že by zjistil že z uvedeného lze dokázat libovolnou formuli, a tím pádem jedna z uvedených formulí není pravdivá v kontextu ostatních, a jelikož A-3 a MP víme že jsou OK, musí být not(not(v7)) dokazatelné?keff píše: a) jak Prover pozná že MP může použít a v7 má dokázat, když mají ty dva řádky stejou syntax?
Re: iny druh domacej
Prover hleda spor - tzn. snazi se ze zadanych formuli odvodit formuli ktera bude negaci nejaky formule co jsem mu zadal. Snazi se pouzit vsechny zadany formule, ale ta negace (v7) mu asi k nicemu neni. Zato pomoci MP odvodi spoustu formuli, az odvodi (v7) P(i(i(n(a),a),a), a to je spor s -P(i(i(n(a),a),a). Tak si to predstavuju ja, ale mozna ze ve skutecnosti to je jinak.keff píše: Můžu ještě využít tvé know-how pro vysvětlení techle dvou řádků?
a) jak Prover pozná že MP může použít a v7 má dokázat, když mají ty dva řádky stejopu syntax?
Tak nejak, ale mozna bych prohodil poradi:keff píše: b) řádek s MP znamená 'y platí, nebo x neplatí, nebo implikace x->y je nepravdivá'?
Neplati 'x->y' nebo neplati 'x' nebo plati 'y'.
Re: iny druh domacej
Cau,Lucas píše:Zdravim.
Ja mam tiez tazku hlavu zo zapoctovej ulohy..
A bol by som aj ochotny podporit vasu ochotu pomoct cloveku v nudzi .. =) .. nejakou odmenou.
Moj priklad:
Uvažujte následující formální systém pro výrokovou logiku s jednou binární logickou spojkou d:
schéma axiomu L: (d(P,d(Q,R)),d(d(P,d(R,P)),d(d(S,Q),d(d(P,S),d(P,S)))))
odvozovaci pravidlo N: Pokud platí d(P,d(Q,R)) a P, pak platí R.
Nalezněte sémantiku tohoto systému (významovou interpretaci spojek a proměnných. Z přednášky například znáte sémantiku pro výrokovou logiku k systém axiomů A1,A2,A3 a pravidla MP) a formálně dokažte, že je korektní.
Lebo I have no f. idea...
pliiiis
asi mas najit takove zobrazeni d:{0,1}x{0,1}-->{0,1} aby zadany axiom byl tautologii pro kazde ohodnoceni promennych P,Q,R,S z mnoziny pravd. hodnot {0,1} a aby taky platilo odvozovaci pravidlo (pro kazde ohodnoceni P,Q,R z {0,1}: pokud plati d(P,d(Q,R))=1 a P=1, potom musi platit i R=1).
Takze je treba najit:
d(0,0)=?
d(0,1)=?
d(1,0)=?
d(1,1)=?
To je celkem 2^4=16 moznosti k pro zkouseni. Osobne bych to asi zkusel testovat v delphi, neco jako:
Kód: Vybrat vše
function d(a,b:boolean):boolean;
begin
{ misto tech otazniku zkousej ruzny moznosti:
0,0,0,0
0,0,0,1
0,0,1,0
0,0,1,1
...
1,1,1,0
1,1,1,1
}
if not a and not b then d:=?;
if not a and b then d:=?;
if a and not b then d:=?;
if a and b then d:=?;
end;
function je_axiom_tautologie: boolean;
var
P,Q,R,S:boolean;
begin
je_axiom_tautologie:=true;
for P:=false to true do
for Q:=false to true do
for R:=false to true do
for S:=false to true do
begin
if not d(d(P,d(Q,R)),d(d(P,d(R,P)),d(d(S,Q),d(d(P,S),d(P,S))))) then
begin
je_axiom_tautologie:=false;
break;
end;
end;
{na to odvozovaci pravidlo uz nemam silu sorry :-) }
Re: iny druh domacej
Wow, díky moc, Prover se sice hodinu potil, ale vypotil formální důkaz o 50ti krocích, takže to asi nebylo myšleno pro ruční počítání .jirka_v píše:...
Jupíí, už to jen přepsat do formyco mají logici rádi a je to
Re: iny druh domacej
Parada . Rado se stalo.keff píše: Wow, díky moc, Prover se sice hodinu potil, ale vypotil formální důkaz o 50ti krocích, takže to asi nebylo myšleno pro ruční počítání .
Jupíí, už to jen přepsat do formyco mají logici rádi a je to
Re: iny druh domacej
Napsal by si sem prosím jak vypadal ten vstup pro proover a jak si to pak přepsal? + co na to případně vyskočil, když chce i zdroják pokud to budem řešit kompem. Mám velmi podobnej úkol. Předem díkkeff píše:Wow, díky moc, Prover se sice hodinu potil, ale vypotil formální důkaz o 50ti krocích, takže to asi nebylo myšleno pro ruční počítání .jirka_v píše:...
Jupíí, už to jen přepsat do formyco mají logici rádi a je to