Zápočtový příklad - Vyskočil

Uživatelský avatar
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

Příspěvek od Lukas Mach »

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.
For every epsilon, there is delta.
Where is my delta?
Uživatelský avatar
tommy
Matfyz(ák|ačka) level I
Příspěvky: 24
Registrován: 1. 6. 2006 13:55

DIKY

Příspěvek od tommy »

Diky velmi pekne. Si nasa zachrana. Idem googlit opisovat prepisovat .. len aby som sa po dlhom case nejak dostal na tu skusku :roll: 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.
Uživatelský avatar
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

Příspěvek od Lucas »

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
Hele mozku, nemáš rád mně a ja zas tebe. Ale tohle musíme udělat a pak tě vyřídim jedním pivem.
keff
Matfyz(ák|ačka) level I
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Re: iny druh domacej

Příspěvek od keff »

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
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?
jirka_v
Matfyz(ák|ačka) level I
Příspěvky: 18
Registrován: 20. 6. 2007 14:20

Re: iny druh domacej

Příspěvek od jirka_v »

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?
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.
keff
Matfyz(ák|ačka) level I
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Re: iny druh domacej

Příspěvek od keff »

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.
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
Matfyz(ák|ačka) level I
Příspěvky: 18
Registrován: 20. 6. 2007 14:20

Re: iny druh domacej

Příspěvek od jirka_v »

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 :).
Neni zac. Pro inspiraci jeste prikladam vstupni soubor pro prover9 k dokazani (v7) v Hilbertove systemu.

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.
keff
Matfyz(ák|ačka) level I
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Re: iny druh domacej

Příspěvek od keff »

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.
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?
b) řádek s MP znamená 'y platí, nebo x neplatí, nebo implikace x->y je nepravdivá'?
keff
Matfyz(ák|ačka) level I
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Re: iny druh domacej

Příspěvek od keff »

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?
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é?
jirka_v
Matfyz(ák|ačka) level I
Příspěvky: 18
Registrován: 20. 6. 2007 14:20

Re: iny druh domacej

Příspěvek od jirka_v »

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?
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: b) řádek s MP znamená 'y platí, nebo x neplatí, nebo implikace x->y je nepravdivá'?
Tak nejak, ale mozna bych prohodil poradi:
Neplati 'x->y' nebo neplati 'x' nebo plati 'y'.
jirka_v
Matfyz(ák|ačka) level I
Příspěvky: 18
Registrován: 20. 6. 2007 14:20

Re: iny druh domacej

Příspěvek od jirka_v »

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
Cau,
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 :-) }
Tak nejak bych hledal tu semantiku (snad to je ok, ruku do ohne bych za to nedal), ale s tim formalnim dukazem korektnosti ti asi nepomuzu. V kazdym pripade doporucuju konzultaci s cvicim. Hodne stesti.
Uživatelský avatar
Lucas
Matfyz(ák|ačka) level I
Příspěvky: 15
Registrován: 15. 1. 2007 20:34
Typ studia: Informatika Mgr.

Příspěvek od Lucas »

Vrelo dik aj zato .. ;-) ..
To hladanie hodnot d(0,0)= ? .. to neviem akou nahodou napadlo aj mne..
Zajtra skusim za nim zajst .. a prekonzultovat to vsetko..
Hele mozku, nemáš rád mně a ja zas tebe. Ale tohle musíme udělat a pak tě vyřídim jedním pivem.
keff
Matfyz(ák|ačka) level I
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Re: iny druh domacej

Příspěvek od keff »

jirka_v 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 :)
jirka_v
Matfyz(ák|ačka) level I
Příspěvky: 18
Registrován: 20. 6. 2007 14:20

Re: iny druh domacej

Příspěvek od jirka_v »

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 :)
Parada :). Rado se stalo.
zoufalec

Re: iny druh domacej

Příspěvek od zoufalec »

keff píše:
jirka_v 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 :)
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ík
Odpovědět

Zpět na „2007“