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

Odeslat odpověď

Smajlíci
:D :) :( :o :shock: :? 8) :lol: :x :P :oops: :cry: :evil: :twisted: :roll: :wink: :!: :?: :idea: :arrow: :| :mrgreen:

BBCode je zapnutý
[img] je zapnutý
[flash] je vypnutý
[url] je zapnuté
Smajlíci jsou zapnutí

Přehled tématu
   

Rozšířit náhled Přehled tématu: Zápočtový příklad - Vyskočil

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

od panther » 29. 9. 2008 00:56

prosím prosím, napište sem někdo jak se cvičící staví k tomu Proveru? Neumím si moc představit jak to řešit bez něj... a potřebuji to velice rychle odevzdat...

od keff » 12. 9. 2007 20:11

Tak to mam, jupiii :)

Re: iny druh domacej

od keff » 8. 9. 2007 01:58

zoufalec píše: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
No, zjistil jsem toho vícero: http://fitelson.org/ar.htmlClassical Sentential Logic --- In the Sheffer Stroke (D):

D je sheffler stroke (NAND)

Nicoduv a Lukasiewiczuv system s jedinym axiomem a jednou logickou spojkou vypada takhle:
In 1917, Nicod [21] showed3 that the following 23-symbol formula (in Polish notation) is a single axiom for classical sentential logic (D is interpreted semantically as NAND, i.e., the Sheffer stroke):

DDpDqrDDtDttDDsqDDpsDps

The only rule of inference for Nicod's single axiom system is the following, somewhat odd, detachment rule for D:

From DpDqr and p, infer r.

Lukasiewicz [7] later showed that the following substitution instance (t/s) of Nicod's axiom (N) would suffice:

DDpDqrDDsDssDDsqDDpsDps


Lukasiewicz's student Mordchaj Wajsberg [37] later discovered the following organic4 23-symbol single axiom for D:

DDpDqrDDDsrDDpsDpsDpDpq

Lukasiewicz later discovered another 23-symbol organic axiom:

DDpDqrDDpDrpDDsqDDpsDps

We have discovered many new 23-symbol single axioms, some of which are organic and have only 4 variables, e.g.,

DDpDqrDDpDqrDDsrDDrsDps

We can now report that the shortest single axioms for these Sheffer Stroke systems contain 23 symbols. No shorter axioms exist.
Ja mam k dispozici dane odvozovaci pravidlo a axiom P(d(d(x,d(y,z)),d(d(x,d(z,y)),d(d(u,y),d(d(x,u),d(x,u)))))) jez se zasobnikove zapise jako DDpDqrDDpDrqDDsqDDpsDps - podezrele se to podoba predchozim... ale vcelku jsem si krome zajimaveho pocteni tolik nepomohl, narozdil od nekoho kdo mel k tomuhle systemu najit semantiku (mam u tebe aspon pivo :)). Porad jeste z toho musim dokazat tu megaformuli s Proverovskym dlouhym dukazem ktery se prepisuje do formalni logiky dosti nepohodlne - nejake zkusenosti anyone?[/quote]

Re: iny druh domacej

od Lukas Mach » 6. 9. 2007 15:33

jirka_v píše:Pro inspiraci jeste prikladam vstupni soubor pro prover9 k dokazani (v7) v Hilbertove systemu.
Diky, tohle jsem v tom proveru nemel energii hledat. Kazdopadne hlasim, ze pred chvili mi Vyskocil dal zapocet (reseni jsem odevzal presne takove, jake jsem popsal v prvni prispevku).

Re: iny druh domacej

od zoufalec » 4. 9. 2007 21:58

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

Re: iny druh domacej

od jirka_v » 4. 9. 2007 16:28

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.

Re: iny druh domacej

od keff » 4. 9. 2007 15:37

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 :)

od Lucas » 3. 9. 2007 20:23

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..

Re: iny druh domacej

od jirka_v » 3. 9. 2007 16:34

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.

Re: iny druh domacej

od jirka_v » 3. 9. 2007 13:51

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'.

Re: iny druh domacej

od keff » 3. 9. 2007 13:46

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é?

Re: iny druh domacej

od keff » 3. 9. 2007 13:41

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á'?

Re: iny druh domacej

od jirka_v » 3. 9. 2007 13:35

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.

Re: iny druh domacej

od keff » 3. 9. 2007 13:27

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 :).

Re: iny druh domacej

od jirka_v » 3. 9. 2007 13:19

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.

Nahoru