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.
[quote="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[/quote]
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:
[code]
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 :-) }
[/code]
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.