Pr ktorecBasismènoisth Gn¸sh - UoAcgi.di.uoa.gr/~ys02/dialekseis2011/propositional2spp.pdf ·...

Teqnht NohmosÔnh M. Koumpar�khc'

&

$

%

Pr�ktorec Basismènoi sth Gn¸sh

• Basikèc ènnoiec

• Gl¸ssec anapar�stashc gn¸shc basismènec sth Logik

• Protasiak logik


&

$

%


O sqediasmìc enìc pr�ktora basismènou sth gn¸sh(knowledge-based agent) basÐzetai stic ex c upojèseic:

• H ènnoia thc gn¸shc eÐnai prwtarqik .

• EÐnai aparaÐthto na èqoume rht anapar�stash thc gn¸shcpou apaiteÐtai gia thn epÐlush enìc probl matoc eswterik�ston pr�ktora.

• H epilog twn enèrgeiwn tou pr�ktora gÐnetai me th bo jeiamiac diadikasÐac sumperasmoÔ (inference) sullogistik c(reasoning) pou efarmìzetai sthn anapar�stash thc gn¸shcpou up�rqei eswterik� ston pr�ktora.


&

$

%

Basikèc 'Ennoiec

• H gl¸ssa anapar�stashc gn¸shc (knowledgerepresentation language): eÐnai h gl¸ssa sthn opoÐaekfr�zetai h gn¸sh sqetik me ton kìsmo tou pr�ktora.

• H b�sh gn¸shc (knowledge base): eÐnai èna sÔnoloprot�sewn thc gl¸ssac anapar�stashc gn¸shc pouparist�noun th gn¸sh tou pr�ktora gia ton kìsmo tou.

H b�sh gn¸shc eÐnai h eswterik anapar�stash thc gn¸shcpou up�rqei ston pr�ktora.


&

$

%

Basikèc 'Ennoiec

• O mhqanismìc sumperasmoÔ sullogistik c: eÐnai ènacmhqanismìc o opoÐoc kajorÐzei ti èpetai logik� apì th gn¸shsth b�sh gn¸sewn.

• H diepaf enhmer¸sewn TELL kai erwt sewn ASK: hdiepaf aut perilamb�nei leitourgÐec gia eisagwg nèwnprot�sewn sth b�sh gn¸shc kai thn diatÔpwsh erwt sewn seìti eÐnai dh gnwstì.

Aut h leitourgÐa eÐnai parìmoia me thn upobol enhmer¸sewnkai erwt sewn se mia b�sh dedomènwn.

H leitourgÐa ASK qrhsimopoieÐ to mhqanismì sumperasmoÔ giana breÐ thn ap�nthsh se mia er¸thsh.


&

$

%

Genikìc Pr�ktorac Basismènoc sth Gn¸sh

function KB-Agent(percept) returns an action

static KB, b�sh gn¸shct, metrht c gia to qrìno, arqik� 0

Tell(KB,Make-Percept-Sentence(percept, t))action ← Ask(KB,Make-Action-Query(t))Tell(KB,Make-Action-Sentence(action, t))t ← t + 1return action


&

$

%


'Enac pr�ktorac basismènoc se gn¸sh mporeÐ na perigrafeÐ se trÐa epÐpeda:

• EpÐpedo gn¸shc (knowledge level): Se autì to epÐpedo opr�ktorac prosdiorÐzetai lègontac ti gnwrÐzei gia ton kìsmo kai poioÐeÐnai oi stìqoi tou.

• Logikì epÐpedo (logical level): Autì eÐnai to epÐpedo sto opoÐo hgn¸sh kai oi stìqoi tou pr�ktora kwdikopoioÔntai se prot�seick�poiac logik c gl¸ssac.

• EpÐpedo ulopoÐhshc (implementation level): Autì eÐnai toepÐpedo sto opoÐo oi prot�seic ulopoioÔntai apì èna prìgramma poutrèqei p�nw sthn arqitektonik tou pr�ktora.

ShmeÐwsh: Antiparab�lete th dhlwtik (declarative) me thdiadikastik (procedural) prosèggish sthn ulopoÐhsh tou sust matoc.


&

$

%

Par�deigma: Autìmatoc Odhgìc TaxÐ

• EpÐpedo gn¸shc:O autìmatoc odhgìc taxÐ gnwrÐzei ìti h gèfura tou GoldenGate sundèei to San Francisco me to Marin County.

• Logikì epÐpedo:O autìmatoc odhgìc taxÐ èqei thn prìtash thc logik pr¸thct�xhc Links(GGBridge,SF,Marin) sth b�sh gn¸shc tou.

• EpÐpedo ulopoÐhshc:H prìtash Links(GGBridge,SF,Marin) ulopoieÐtai apì miadom thc C èna gegonìc (fact) thc Prolog.


&

$

%

Autìnomoi Pr�ktorec Basismènoi sth Gn¸sh

MporoÔme na qtÐsoume ènan pr�ktora basismèno se gn¸shenhmer¸nont�c ton ti qrei�zetai na gnwrÐzei prin arqÐsei naantilamb�netai ton kìsmo (qrhsimopoi¸ntac thn TELL).

MporoÔme epÐshc na sqedi�soume ènan mhqanismì m�jhshc oopoÐoc ja ex�gei genik gn¸sh gia to perib�llon tou, èqontac wcdedomèna mia seir� apì pr�gmata pou èqei antilhfjeÐ.

Autìnomoc pr�ktorac = Pr�ktorac basismènoc se gn¸sh+ Mhqanismìc m�jhshc


&

$

%

O Kìsmoc tou Wumpus

Breeze Breeze

Breeze

BreezeBreeze

Stench

Stench

BreezePIT

PIT

PIT

1 2 3 4

1

2

3

4

START

Gold

Stench


&

$

%


• Perib�llon: PlaÐsio 4x4 ìpou brÐsketai o pr�ktorac, totèrac Wumpus, mia pl�ka qrusoÔ kai merik� phg�dia.

• MhqanismoÐ dr�shc: O pr�ktorac mporeÐ na kineÐtai mprost�kai na strÐbei dexi� arister�. O pr�ktorac pejaÐnei an mpeisto tetragwn�ki pou brÐsketai to (zwntanì) tèrac pèsei sek�poio phg�di.O pr�ktorac mporeÐ epÐshc na ektelèsei tic enèrgeiec Grab kaiShoot.

• Aisjht rec: H antÐlhyh eÐnai mia lÐsta apì 5 sÔmbola:

(Stench, Breeze, Glitter, Bumb, Scream)

K�je mia apì tic parap�nw timèc mporeÐ na eÐnai None.


&

$

%


ABG

PS

W

= Agent = Breeze = Glitter, Gold

= Pit = Stench

= Wumpus

OK = Safe square

V = Visited

A

OK

1,1 2,1 3,1 4,1

1,2 2,2 3,2 4,2

1,3 2,3 3,3 4,3

1,4 2,4 3,4 4,4

OKOKB

P?

P?A

OK OK

OK

1,1 2,1 3,1 4,1

1,2 2,2 3,2 4,2

1,3 2,3 3,3 4,3

1,4 2,4 3,4 4,4

V

(a) (b)


&

$

%


BB P!

A

OK OK

OK

1,1 2,1 3,1 4,1

1,2 2,2 3,2 4,2

1,3 2,3 3,3 4,3

1,4 2,4 3,4 4,4

V

OK

W!

VP!

A

OK OK

OK

1,1 2,1 3,1 4,1

1,2 2,2 3,2 4,2

1,3 2,3 3,3 4,3

1,4 2,4 3,4 4,4

V

S

OK

W!

V

V V

BS G

P?

P?

(b)(a)

S

ABG

PS

W


= Pit = Stench

= Wumpus

OK = Safe square

V = Visited


&

$

%


Ti qrei�zetai o pr�ktorac gia na epiz sei kai na petÔqei to skopìtou?

• 'Ena mhqanismì antÐlhyhc tou kìsmou.

• 'Ena mhqanismì anapar�stashc gn¸shc (gegonìtwn kaikanìnwn) gia ton kìsmo.

• 'Ena mhqanismì sumperasmoÔ ¸ste apì gnwst� gegonìta naex�goume �gnwsta.


&

$

%


ParadeÐgmata gegonìtwn:

• Aisj�nomai reÔma sto tetragwn�ki [2,1].

• Up�rqei phg�di sto tetragwn�ki [2,2] sto tetragwn�ki [3,1].

• Den up�rqei phg�di sto tetragwn�ki [2,2].

Par�deigma kanìna:

• An se èna tetragwn�ki aisj�nesai reÔma, tìte s' èna apì tadiplan� tetragwn�kia up�rqei phg�di.

Par�deigma sumperasmoÔ:

• AfoÔ sto tetragwn�ki [2,1] aisj�nomai reÔma, tìte up�rqeiphg�di sto tetragwn�ki [2,2] sto tetragwn�ki [3,1] (me b�shton parap�nw kanìna).


&

$

%

H Sunèqeia

Sth sunèqeia tou maj matoc ja melet soume dÔo gl¸ssecanapar�stashc gn¸shc kai ja orÐsoume antÐstoiqoucmhqanismoÔc sumperasmoÔ.

Oi gl¸ssec autèc ja mporoÔn na qrhsimopoihjoÔn giaanapar�stash gn¸shc sto kìsmo tou Wumpus.


&

$

%

Gl¸ssec Anapar�stashc Gn¸shc

Mia gl¸ssa anapar�stashc gn¸shc orÐzetai prosdiorÐzontac tosuntaktikì (syntax) kai th shmasiologÐa thc (semantics).

To suntaktikì miac gl¸ssac anapar�stashc gn¸shc kajorÐzei meakrÐbeia touc kal� orismènouc tÔpouc kai prot�seic thc gl¸ssac.

H shmasiologÐa miac gl¸ssac anapar�stashc gn¸shc orÐzei thnantistoiqÐa metaxÔ twn tÔpwn/prot�sewn thc gl¸ssac kai twngegonìtwn tou kìsmou ston opoÐo anafèrontai oi tÔpoi/prot�seic.


&

$

%

ErmhneÐa - AlhjeÐc Prot�seic

Mia prìtash miac gl¸ssac anapar�stashc gn¸shc den shmaÐneitÐpota apì mình thc. H shmasiologÐa (dhlad h shmasÐa) thcprotashc prèpei na parèqetai apì ton suggrafèa thc me th morf miac ermhneÐac (interpretation).

AlhjeÐc prot�seic. Mia prìtash ja lègetai alhj c (true) semia sugkekrimènh ermhneÐa an h kat�stash pou perigr�fei hprìtash isqÔei sthn ermhneÐa.


&

$

%

Logik K�luyh (Entailment)

Ja gr�foumeKB |= α

gia na dhl¸soume ìti opoted pote oi prot�seic thc KB eÐnaialhjeÐc, tìte h prìtash α eÐnai epÐshc alhj c. S' aut thnperÐptwsh ja lème ìti oi prot�seic thc KB kalÔptoun logik�thn prìtash α ( ìti h α èpetai logik� apì thn KB ìti h α

eÐnai logik sunèpeia thc KB).

Dedomènhc miac KB kai miac prìtashc α, p¸c mporoÔme nasqedi�soume ènan algìrijmo o opoÐoc ja epalhjeÔei an isqÔeiKB |= α?


&

$

%

O Rìloc thc ShmasiologÐac

Follows

Sentences SentenceEntails

Se

ma

ntics

Sem

an

tics

Representation

World

Aspects of the real world

Aspect of the real world


&

$

%

Sumperasmìc

Sumperasmìc (inference) eÐnai h diadikasÐa exagwg c prot�sewnpou èpontai logik� apì mia b�sh gn¸shc me mhqanikì trìpo. Anmia prìtash α par�getai apì thn KB qrhsimopoi¸ntac ènamhqanismì sumperasmoÔ i tìte gr�foume KB `i α.

'Enac mhqanismìc sumperasmoÔ kaleÐtai orjìc (sound) an par�geimìno prot�seic pou èpontai logik�.

'Enac mhqanismìc sumperasmoÔ kaleÐtai pl rhc (complete) anpar�gei ìlec tic prot�seic pou èpontai logik�.


&

$

%

JewrÐa ApodeÐxewn - Kanìnec SumperasmoÔ

To sÔnolo twn bhm�twn pou akoloujoÔntai gia na paraqjeÐ mia nèaprìtash α apì to sÔnolo prot�sewn miac b�shc gn¸shc KB

kaleÐtai apìdeixh (proof).

Mia jewrÐa apodeÐxewn (proof theory) eÐnai èna sÔnolokanìnwn pou qrhsimopoioÔntai gia thn exagwg prot�sewn pouèpontai logik� apì èna �llo sÔnolo prot�sewn (mia b�shgn¸sewn). Oi kanìnec autoÐ lègontai kanìnec sumperasmoÔ(inference rules).


&

$

%

Logik

Oi gl¸ssec anapar�stashc gn¸shc pou ja melet soume eÐnai:

• H protasiak logik (propositional logic) logik touBoole (Boolean logic).

• H logik pr¸thc t�xhc (first-order logic).

'Etsi oi pr�ktorec basismènoi sth gn¸sh pou ja dhmiourg soume jaonom�zontai logikoÐ pr�ktorec (logical agents).


&

$

%

Logik

Genik� mia logik (logic) eÐnai èna tupikì sÔsthma pou apoteleÐtaiapì:

• Suntaktikì (Syntax)

• ShmasiologÐa (Semantics)

• JewrÐa apodeÐxewn (Proof theory)

Er¸thsh: GiatÐ qrhsimopoioÔme gl¸ssec logik c gia thnanapar�stash gn¸shc? GiatÐ na mhn qrhsimopoi soume fusik gl¸ssa k�poia gl¸ssa programmatismoÔ?


&

$

%

Protasiak Logik : Suntaktikì

Ta sÔmbola thc protasiak c logik c eÐnai:

• Oi stajerèc True kai False.

• 'Ena arijm simo apeirosÔnolo protasiak¸n sumbìlwn(proposition symbols) P1, P2, . . . Autì to sÔnolo jasumbolÐzetai me P.

• Oi logikoÐ sÔndesmoi: ¬,∧,∨,⇒ kai ⇔.

• Oi parenjèseic: (, ).


&

$

%

Proteraiìthta

Den up�rqoun apodektoÐ ap' ìlouc kanìnec proteraiìthtactelest¸n gia thn protasiak logik .

H proteraiìthta (apì th megalÔterh proc th mikrìterh) pou jaqrhsimopoi soume akolouj¸ntac to biblÐo AIMA eÐnai: ¬,∧,∨,⇒kai ⇔.

'An èqete amfibolÐa gia thn proteraiìthta, tìte qrhsimopoieÐsteparenjèseic. Epitrèpontai kai oi agkÔlec ¸ste na exasfalÐzetaih anagnwsimìthta miac prìtashc.


&

$

%

ParadeÐgmata

• H prìtash P ∧Q ∨R eÐnai isodÔnamh me thn (P ∧Q) ∨R.

• H prìtash ¬P ∨Q ∧R ⇒ S eÐnai isodÔnamh me thn(¬(P ) ∨ (Q ∧R)) ⇒ S.

H prìtash A ∧B ∧ C (ìpou h proteraiìthta den bohj�ei) mporeÐ nadiabasteÐ san (A ∧B) ∧ C A ∧ (B ∧ C) qwrÐc prìblhma lìgwisodunamÐac twn tri¸n aut¸n prot�sewn (ja orÐsoume me akrÐbeiathn ènnoia thc isodunamÐac parak�tw).

OmoÐwc gia touc sÔndesmouc ∨ kai ⇔, all� ìqi gia ton ⇒. Prèpeidhlad na qrhsimopoi soume parenjèseic sthn prìtashA ⇒ B ⇒ C.


&

$

%

Protasiak Logik : Ontologikèc Upojèseic

Oi ontologikèc upojèseic miac logik c sqetÐzontai me th fÔshtwn kìsmwn pou mporoÔn na anaparastajoÔn apì th sugkrekrimènhlogik .

H protasiak logik upojètei ìti o kìsmoc apoteleÐtai apìgegonìta (facts) ta opoÐa eÐte alhjeÔoun eÐte denalhjeÔoun.

H logik pr¸thc t�xhc pou epekteÐnei thn protasiak logik k�neipio polÔplokec kai leptomereÐc ontologikèc upojèseic.

H basik upìjesh ìti èna gegonìc eÐnai alhjèc yeudèc denisqÔei se �llec logikèc p.q. thn asaf logik (fuzzy logic).


&

$

%

Protasiak Logik : ShmasiologÐa

Follows

Sentences SentenceEntails

Se

ma

ntics

Sem

an

tics

Representation

World

Aspects of the real world

Aspect of the real world


&

$

%


'Ena protasiakì sÔmbolo (proposition symbol) mporeÐ naparist�nei otid pote jèloume. H ermhneÐa tou mporeÐ na eÐnai ènaopoiod pote gegonìc. 'Omwc to gegonìc autì prèpei na eÐnai eÐtealhjèc eÐte yeudèc ston kìsmo pou montelopoioÔme.

Ta parap�nw diatup¸nontai tupik� eis�gontac thn ènnoia thcermhneÐac.

Orismìc. 'Estw P èna sÔnolo protasiak¸n sumbìlwn. MiaermhneÐa (interpretation) gia to P eÐnai mia apeikìnish

I : P → {false, true}.


&

$

%


H ènnoia thc ermhneÐac mporeÐ na epektajeÐ se ìlec tic kal�orismènec prot�seic thc protasiak c logik c akolouj¸ntac toucex c anadromikoÔc orismoÔc:

• I(True) = true.

• I(False) = false.

• I(¬φ) = true an I(φ) = false, diaforetik� I(¬φ) = false.

• I(φ1 ∧ φ2) = true an I(φ1) = true kai I(φ2) = true,diaforetik� I(φ1 ∧ φ2) = false.

• I(φ1 ∨ φ2) = true an I(φ1) = true I(φ2) = true, diaforetik�I(φ1 ∨ φ2) = false.


&

$

%


• I(φ1 ⇒ φ2) = true an I(φ1) = false I(φ2) = true,diaforetik� I(φ1 ⇒ φ2) = false.

• I(φ1 ⇔ φ2) = true an I(φ1) = I(φ2), diaforetik�I(φ1 ⇔ φ2) = false.


&

$

%

Par�deigma: O Kìsmoc tou Wumpus

Breeze Breeze

Breeze

BreezeBreeze

Stench

Stench

BreezePIT

PIT

PIT

1 2 3 4

1

2

3

4

START

Gold

Stench


&

$

%

Anapar�stash me Protasiak Logik

Ja qrhsimopoi soume ta ex c protasiak� sÔmbola gia na parast soumemerikèc apì tic gn¸seic pou èqoume gia to kìsmo tou Wumpus ìpwc autècdÐnontai sthn prohgoÔmenh eikìna:

• O pr�ktorac eÐnai sto tetragwn�ki [x, y]: Axy

• O Wumpus eÐnai sto tetragwn�ki [x, y]: Wxy

• Up�rqei phg�di sto tetragwn�ki [x, y]: Pxy

• Up�rqei aÔra sto tetragwn�ki [x, y]: Bxy


&

$

%

Anapar�stash me Protasiak Logik

Sthn prohgoÔmenh eikìna, me b�sh to sumbolismì mac, mporoÔme diaisjhtik�na poÔme ìti oi parak�tw prot�seic �isqÔoun�:

A11, W31, P13, P33, P44, B43, B32, B34, B34, B23, B12, B14,

¬A12, ¬W11, ¬(P44 ∧A44)


&

$

%

Mia Kat�llhlh ErmhneÐa

Mia kat�llhlh ermhneÐa I gia ta protasiak� sÔmbola mac pou kwdikopoieÐì,ti blèpoume sqetik� me aut� ta sÔmbola sthn prohgoÔmenh eikìnakajorÐzetai wc ex c:

I(A11) = true, I(Axy) = false gia ìla ta �lla zeÔgh x, y

I(W31) = true, I(Wxy) = false gia ìla ta �lla zeÔgh x, y

I(P13) = true, I(P33) = true, I(P44) = true,

I(Pxy) = false gia ìla ta �lla zeÔgh x, y

I(B43) = true, I(B32) = true, I(B34) = true, I(B34) = true,

I(B23) = true, I(B12) = true, I(B14) = true,

I(Bxy) = false gia ìla ta �lla zeÔgh x, y


&

$

%

Poièc Prot�seic IsqÔoun?

MporoÔme t¸ra na doÔme poièc prot�seic �isqÔoun� diaisjhtik� sthn eikìnapou eÐdame. EÐnai autèc pou h ermhneÐa I touc dÐnei thn tim true. Giapar�deigma:

I(¬A12) = true, I(¬W11) = true, I(¬(P44 ∧A44)) = true,

I(A11 ⇒ ¬W11) = true, I(A13 ⇒ W11) = true

AntÐjeta, oi parak�tw prot�seic stic opoÐec h ermhneÐa dÐnei thn tim false,den �isqÔoun":

I(¬A11) = false, I(P43 ∨A44) = false, I(P44 ⇒ (W11 ∨A12)) = false


&

$

%

'Allec ErmhneÐec

Up�rqoun �llec ermhneÐec gia ta protasiak� sÔmbola mac pou denantistoiqoÔn sthn prohgoÔmenh eikìna. Gia par�deigma h parak�tw ermhneÐaJ :

J(A44) = true, J(Axy) = false gia ìla ta �lla zeÔgh x, y

J(W31) = true, J(Wxy) = false gia ìla ta �lla zeÔgh x, y

J(P13) = true, J(P33) = true, J(P44) = true,

J(Pxy) = false gia ìla ta �lla zeÔgh x, y

J(B43) = true, J(B32) = true, J(B34) = true, J(B34) = true,

J(B23) = true, J(B12) = true, J(B14) = true,

J(Bxy) = false gia ìla ta �lla zeÔgh x, y


&

$

%

Sunjetikìthta thc Protasiak c Logik c

Mia gl¸ssa kaleÐtai sunjetik (compositional) ìtan h shmasÐamiac prìtashc thc gl¸ssac eÐnai sun�rthsh thc shmasÐac twntmhm�twn aut c thc prìtashc.

H sunjetikìthta eÐnai mia epijumht idiìthta stic tupikèc gl¸ssec.

H protasiak logik èqei thn idiìthta thc sunjetikìthtac ìpwcmporoÔme na doÔme apì touc orismoÔc thc shmasiologÐac thc.


&

$

%

IkanopoÐhsh - Montèlo

Orismìc. 'Estw φ mia prìtash thc protasiak c logik c. An I

eÐnai mia ermhneÐa tètoia ¸ste I(φ) = true tìte lème ìti I

ikanopoieÐ (satisfies) th φ ìti h I eÐnai èna montèlo (model)thc φ.


&

$

%

Par�deigma

H ermhneÐa I pou d¸same nwrÐtera ikanopoieÐ tic parak�twprot�seic:

True, ¬A12, ¬W11, ¬(P44 ∧A44),

A11 ⇒ ¬W11, A13 ⇒ W11

H ermhneÐa I den ikanopoieÐ tic parak�tw prot�seic:

False, ¬A11, P43 ∨A44, P44 ⇒ (W11 ∨A12)


&

$

%

Ikanopoihsimìthta

Orismìc. Mia prìtash φ thc protasiak c logik c eÐnaiikanopoi simh (satisfiable) an up�rqei mia ermhneÐa I tètoia¸ste I(φ) = true.

ParadeÐgmata: P, P ∨Q, (P ∧R) ∨Q

Orismìc. Mia prìtash φ thc protasiak c logik c eÐnai mhikanopoi simh (unsatisfiable) an den up�rqei kamÐa ermhneÐa I

tètoia ¸ste I(φ) = true.

Par�deigma: P ∧ ¬P


&

$

%

Egkurìthta (Validity)

Orismìc. Mia prìtash φ thc protasiak c logik c eÐnai ègkurh (valid)an gia k�je ermhneÐa I, isqÔei I(φ) = true.

ParadeÐgmata: P ∨ ¬P , ((P ∨H) ∧ ¬H) ⇒ P

Oi ègkurec prot�seic thc protasiak c logik c lègontai kai tautologÐec(tautologies).

Je¸rhma. 'Estw φ mia prìtash thc protasiak c logik c. H φ eÐnai mhikanopoi simh ann h ¬φ eÐnai ègkurh. Apìdeixh?

Prosoq : �ann� shmaÐnei �an kai mìno an�


&

$

%

H GewgrafÐa thc Protasiak c Logik c

Satisfiable Sentences

Unsatisfiable Sentences

Valid Sentences


&

$

%

Logik K�luyh (Entailment)

Orismìc. 'Estw φ kai ψ prot�seic thc protasiak c logik c. Ja lème ìtih φ kalÔptei logik� (entails) thn ψ ìti h ψ èpetai logik� apì thn φ

ìti h ψ eÐnai logik sunèpeia thc φ (sumbolismìc: φ |= ψ) an gia k�jeermhneÐa I tètoia ¸ste I(φ) = true isqÔei ìti I(ψ) = true.

ParadeÐgmata: P ∧Q |= P, P ∧ (P ⇒ Q) |= Q

Je¸rhma Paragwg c (Deduction Theorem). 'Estw φ kai ψ

prot�seic thc protasiak c logik c. Tìte φ |= ψ ann φ ⇒ ψ eÐnai ègkurh.Apìdeixh?


&

$

%

Logik K�luyh kai Mh Ikanopoihsimìthta

Je¸rhma. 'Estw φ kai ψ prot�seic thc protasiak c logik c.Tìte φ |= ψ ann φ ∧ ¬ψ eÐnai mh ikanopoi simh. Apìdeixh?

To parap�nw je¸rhma eÐnai h b�sh twn apodeÐxewn me apagwg se �topo (se qr sh apì thn epoq tou Aristotèlh).


&

$

%

IsodunamÐa

Orismìc. 'Estw φ kai ψ prot�seic thc protasiak c logik c. Jalème ìti h φ eÐnai isodÔnamh (equivalent) me thn ψ

(sumbolismìc: φ ≡ ψ) an φ |= ψ kai ψ |= φ.

Par�deigma: ¬(P ∧ ¬Q) ≡ ¬P ∨Q

Je¸rhma. φ ≡ ψ ann h prìtash φ ⇔ ψ eÐnai ègkurh. Apìdeixh?


&

$

%

Merikèc Qr simec IsodunamÐec

'Estw α, β kai γ prot�seic thc protasiak c logik c. Tìte:

• (α ∧ β) ≡ (β ∧ α) antimetajetikìthta tou ∧• (α ∨ β) ≡ (β ∨ α) antimetajetikìthta tou ∨• ((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ)) prosetairistikìthta tou ∧• ((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ)) prosetairistikìthta tou ∨• ¬(¬α) ≡ α apaloif dipl c �rnhshc

• (α ⇒ β) ≡ (¬β ⇒ ¬α) antijetoantistrof (contraposition)


&

$

%

Merikèc Qr simec IsodunamÐec

• (α ⇒ β) ≡ (¬α ∨ β) apaloif sunepagwg c

• (α ⇔ β) ≡ ((α ⇒ β) ∧ (β ⇒ α)) apaloif dipl csunepagwg c

• ¬(α ∧ β) ≡ (¬α ∨ ¬β) nìmoc de Morgan

• ¬(α ∨ β) ≡ (¬α ∧ ¬β) nìmoc de Morgan

• (α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ)) epimeristikìthta tou ∧ wcproc to ∨

• (α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ)) epimeristikìthta tou ∨ wcproc to ∧


&

$

%

PÐnakec AlhjeÐac

Oi pÐnakec alhjeÐac (truth tables) eÐnai ergaleÐa pou macepitrèpoun na broÔme thn tim alhjeÐac miac prìtashc thcprotasiak c logik c an gnwrÐzoume tic timèc alhjeÐac twn epimèroucprot�sewn pou thn apartÐzoun (me b�sh th sunjesimìthta thcprotasiak c logik c).


&

$

%

PÐnakec AlhjeÐac

A ¬A

true false

false true

A B A ∧B A ∨B A ⇒ B A ⇔ B

false false false false true true

false true false true true false

true false false true false false

true true true true true true


&

$

%

PÐnakec AlhjeÐac: GiatÐ EÐnai Qr simoi?

• Oi pÐnakec alhjeÐac mporoÔn na qrhsimopoihjoÔn gia naapodeÐxoume thn al jeia to yeÔdoc miac opoiasd poteprìtashc thc protasiak c logik c se mia dedomènh ermhneÐa.

• ParomoÐwc, oi pÐnakec alhjeÐac mporoÔn na qrhsimopoihjoÔngia na apodeÐxoume thn ikanopoihsimìthta thn egkurìthtamiac prìtashc, thn isodunamÐa dÔo prot�sewn thcprotasiak c logik c.

• Upologistik Poluplokìthta: O(2n) ìpou n eÐnai oarijmìc twn protasiak¸n sumbìlwn thc prìtashc.


&

$

%

Par�deigma

PÐnakac alhjeÐac gia na apodeÐxoume thn egkurìthta thc prìtashc((P ∨H) ∧ ¬H) ⇒ P .

P H P ∨H (P ∨H) ∧ ¬H ((P ∨H) ∧ ¬H)

⇒ P

false false false false true

false true true false true

true false true true true

true true true false true


&

$

%

Par�deigma

'Enac pÐnakac alhjeÐac pou deÐqnei ìti { P ∨H, ¬H } |= P .

P H P ∨H ¬H P

false false false true false

false true true false false

true false true true true

true true true false true


&

$

%

JewrÐa ApodeÐxewn kai Kanìnec SumperasmoÔ

'Enac kanìnac sumperasmoÔ (inference rule) eÐnai ènackanìnac thc morf c

α1, α2, . . . , αn

β

ìpou α1, α2, . . . , αn eÐnai prot�seic oi opoÐec onom�zontaiupojèseic kai β eÐnai mia prìtash pou onom�zetai sumpèrasma.

'Enac kanìnac sumperasmoÔ efarmìzetai wc ex c: opoted poteèqoume èna sÔnolo prot�sewn pou tairi�zoun me tic upojèseic toukanìna, mporoÔme na ex�goume thn prìtash-sumpèrasma.


&

$

%

Protasiak Logik : Kanìnec SumperasmoÔ

• Trìpoc tou jètein (modus ponens): α⇒β, αβ

• Apaloif sÔzeuxhc: α1∧α2∧...∧αn

αi

• Eisagwg sÔzeuxhc: α1,α2,...,αn

α1∧α2∧...∧αn

• Eisagwg di�zeuxhc: αi

α1∨α2∨...∨αn

• Apaloif dipl c �rnhshc: ¬¬αα

• MonadiaÐa an�lush: α∨β, ¬βα

• An�lush: α∨β, ¬β∨γα∨γ


&

$

%

Protasiak Logik : Mèjodoi ApodeÐxewn

H klassik bibliografÐa thc protasiak c logik c perièqei di�forecapodeiktikèc mejìdouc (dhl. tupikèc jewrÐec apodeÐxewn) pou eÐnaiorjèc kai pl reic (p.q., tableaux, Hilbert systems, naturaldeduction systems klp.)

DeÐte gia par�deigma to biblÐo:

Melvin Fitting. First-Order Logic and Automated TheoremProving. Springer, 1996.


&

$

%

GiatÐ EÐnai Shmantikìc o Sumperasmìc?

Wo

rld

input sentences

conclusions

User

?


&

$

%

O Kìsmoc tou Wumpus se Protasiak Logik

ABG

PS

W


= Pit = Stench

= Wumpus

OK = Safe square

V = Visited

A

OK

1,1 2,1 3,1 4,1

1,2 2,2 3,2 4,2

1,3 2,3 3,3 4,3

1,4 2,4 3,4 4,4

OKOKB

P?

P?A

OK OK

OK

1,1 2,1 3,1 4,1

1,2 2,2 3,2 4,2

1,3 2,3 3,3 4,3

1,4 2,4 3,4 4,4

V

(a) (b)


&

$

%

O Kìsmoc tou Wumpus se Protasiak Logik

H b�sh gn¸shc gia thn eikìna (a):

• Den up�rqei phg�di sto [1, 1] (antÐlhyh tou pr�ktora):

R1 : ¬P11

• S' èna tetragwn�ki gÐnetai antilhpt aÔra an kai mìno an up�rqeiphg�di se geitonikì tetragwn�ki (kanìnac tou kìsmou).Diatup¸noume autìn ton kanìna mìno gia to tetragwn�ki [1, 1]:

R2 : B11 ⇔ P12 ∨ P21

• De gÐnetai antilhpt aÔra sto tetragwn�ki [1, 1] (antÐlhyh toupr�ktora).

R3 : ¬B11


&

$

%

Sumperasmìc ston Kìsmo tou Wumpus

O pr�ktorac mporeÐ t¸ra na qrhsimopoi sei touc kanìnecsumperasmoÔ thc protasiak c logik c kai tic logikècisodunamÐec gia na apodeÐxei to ex c:

Den up�rqei phg�di sta tetragwn�kia [1, 2] [2, 1].

• Efarmìzoume apaloif dipl c sunepagwg c sthn R2:

R4 : (B11 ⇒ (P12 ∨ P21)) ∧ ((P12 ∨ P21) ⇒ B11)

• Efarmìzoume apaloif sÔzeuxhc sthn R4:

R5 : (P12 ∨ P21) ⇒ B11


&

$

%

Sumperasmìc ston Kìsmo tou Wumpus

• Efarmìzoume th logik isodunamÐa gia antijetoantÐstrofecprot�seic sthn R5:

R6 : ¬B11 ⇒ ¬(P12 ∨ P21)

• Efarmìzoume modus ponens stic R6 kai R3:

R7 : ¬(P12 ∨ P21)

• Efarmìzoume ton kanìna de Morgan sthn R7 kai èqoume toepijumhtì sumpèrasma:

R8 : ¬P12 ∧ ¬P21


&

$

%

H Idiìthta thc Monotonikìthtac

H protasiak logik (ìpwc kai h logik pr¸thc t�xhc pou ja doÔmeargìtera) eÐnai monìtonh:

An KB |= φ tìte KB ∧ ψ |= φ.

Autì shmaÐnei ìti an prostejeÐ nèa gn¸sh ψ se mia b�sh gn¸sewnKB tìte mporoÔme pijan� na sumper�noume nèa gn¸sh, all� denmporoÔme na akur¸soume gn¸sh pou dh eÐqame sumper�nei apì thnKB.


&

$

%

O Kanìnac SumperasmoÔ thc An�lushc

Ja parousi�soume t¸ra ton kanìna sumperasmoÔ thc an�lushc poueÐnai ènac orjìc kai pl rhc kanìnac sumperasmoÔ gia thnprotasiak logik .

Gia na efarmìsoume ton kanìna thc an�lushc, oi prot�seic thcprotasiak c logik c prèpei na eÐnai se suzeuktik kanonik morf .

DÐnoume amèswc touc sqetikoÔc orismoÔc.


&

$

%

Lektik� (Literals)

Orismìc. 'Ena lektikì (literal) eÐnai èna protasiakì sÔmbolo h �rnhsh tou. Sthn pr¸th perÐptwsh èqoume èna jetikì lektikìkai sth deÔterh perÐptwsh èna arnhtikì lektikì.

ParadeÐgmata:P1, P2, ¬P3


&

$

%

Fr�seic (Clauses)

Orismìc. Mia fr�sh (clause) eÐnai mia di�zeuxh lektik¸n.

ParadeÐgmata:

P1 ∨ P2 ∨ ¬P3, P1 ∨ P4, ¬P1 ∨ ¬P3 ∨ ¬P5


&

$

%

Suzeuktik Kanonik Morf

Orismìc. Mia prìtash thc protasiak c logik c eÐnai sesuzeuktik kanonik morf (conjunctive normal form,CNF) an eÐnai mia sÔzeuxh fr�sewn (dhl. mia sÔzeuxh diazeÔxewnpou apoteloÔntai apì lektik�).

Je¸rhma. K�je prìtash thc protasiak c logik c mporeÐ nametatrapeÐ se mia isodÔnamh prìtash pou eÐnai se CNF.


&

$

%

Metatrop se CNF

1. Apaloif dipl¸n sunepagwg¸n qrhsimopoi¸ntac thn parak�twisodunamÐa:

(φ ⇔ ψ) ≡ (φ ⇒ ψ ∧ ψ ⇒ φ)

2. Apaloif apl¸n sunepagwg¸n qrhsimopoi¸ntac thn parak�twisodunamÐa:

φ ⇒ ψ ≡ ¬φ ∨ ψ

3. MetakÐnhsh twn arn sewn (¬) proc ta mèsa ¸ste k�je �rnhshna efarmìzetai se èna atomikì tÔpo. QrhsimopoioÔme tic parak�twisodunamÐec:

¬¬φ ≡ φ

¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ

¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ


&

$

%

Metatrop se CNF

4. Efarmìzoume thn epimeristik idiìthta tou ∨ wc procto ∧:

(φ ∧ ψ) ∨ θ ≡ (φ ∨ θ) ∧ (ψ ∨ θ)

θ ∨ (φ ∧ ψ) ≡ (θ ∨ φ) ∧ (θ ∨ ψ)

5. AplopoioÔme tic suzeÔxeic kai diazeÔxeic apaloÐfontac ticparenjèseic pou den qrei�zontai.

6. ApaloÐfoume to sÔmbolo ∧ kai èqoume mia lÐsta apìdiazeÔxeic (fr�seic).


&

$

%

Par�deigma

'Estw h prìtashP1 ⇔ P2 ∧ ¬(P3 ⇔ P4)

B ma 1:

(P1 ⇒ P2 ∧ P2 ⇒ P1) ∧ ¬(P3 ⇒ P4 ∧ P4 ⇒ P3)

B ma 2:

((¬P1 ∨ P2) ∧ (¬P2 ∨ P1)) ∧ ¬((¬P3 ∨ P4) ∧ (¬P4 ∨ P3))

B ma 3:

((¬P1 ∨ P2) ∧ (¬P2 ∨ P1)) ∧ (¬(¬P3 ∨ P4) ∨ ¬(¬P4 ∨ P3))

((¬P1 ∨ P2) ∧ (¬P2 ∨ P1)) ∧ ((P3 ∧ ¬P4) ∨ (P4 ∧ ¬P3))


&

$

%

Par�deigma

B ma 4:

((¬P1∨P2)∧(¬P2∨P1))∧((P3∨P4)∧(P3∨¬P3)∧(¬P4∨P4)∧(¬P4∨¬P3))

B ma 5:

(¬P1∨P2)∧(¬P2∨P1)∧(P3∨P4)∧(P3∨¬P3)∧(¬P4∨P4)∧(¬P4∨¬P3)

B ma 6:

¬P1 ∨ P2, ¬P2 ∨ P1, P3 ∨ P4, P3 ∨ ¬P3, ¬P4 ∨ P4, ¬P4 ∨ ¬P3


&

$

%

O Kanìnac SumperasmoÔ thc MonadiaÐac An�lushc

O kanìnac sumperasmoÔ thc monadiaÐac an�lushc (unit resolution) giathn protasiak logik eÐnai o ex c.

An li kai m eÐnai sumplhrwmatik� lektik�, tìte:

l1 ∨ · · · ∨ lk, m

l1 ∨ · · · ∨ li−1 ∨ li+1 ∨ · · · ∨ lk

Orismìc. Ta lektik� l kai m lègontai sumplhrwmatik�(complementary) an to èna eÐnai h �rnhsh tou �llou.


&

$

%

Par�deigma

'Estw oi ex c fr�seic:P1 ∨ P2 ∨ ¬P3

¬P2

P3

Apì thn fr�sh P1 ∨ P2 ∨ ¬P3 kai thn P3, me ton kanìna thcmonadiaÐac an�lushc mporoÔme na sumper�noume thn

P1 ∨ P2.

Apì thn fr�sh P1 ∨ P2 kai thn ¬P2 me ton kanìna thc monadiaÐacan�lushc mporoÔme na sumper�noume thn P1.


&

$

%

O Kanìnac SumperasmoÔ thc An�lushc

O kanìnac sumperasmoÔ thc an�lushc (resolution) gia thnprotasiak logik eÐnai o ex c.

An li kai mj eÐnai sumplhrwmatik� lektik�, tìte:

l1 ∨ · · · ∨ lk, m1 ∨ · · · ∨mn

l1 ∨ · · · ∨ li−1 ∨ li+1 ∨ · · · ∨ lk ∨m1 ∨ · · · ∨mj−1 ∨mj+1 ∨ · · ·mn


&

$

%

Par�deigma

'Estw oi ex c fr�seic:P1 ∨ P2 ∨ ¬P3

¬P2 ∨ P1

P3 ∨ P4

Apì thn fr�sh P1 ∨ P2 ∨ ¬P3 kai thn P3 ∨ P4, me ton kanìna thcan�lushc, mporoÔme na sumper�noume thn

P1 ∨ P2 ∨ P4.

Apì thn fr�sh P1 ∨ P2 ∨ P4 kai thn ¬P2 ∨ P1 me ton kanìna thcan�lushc, mporoÔme na sumper�noume thn P1 ∨ P4 ∨ P1. HteleutaÐa fr�sh eÐnai isodÔnamh me thn P1 ∨ P4.


&

$

%

ParagontopoÐhsh (Factoring)

Prèpei na p�nta na afairoÔme tic emfanÐseic pollapl¸n lektik¸napì mia fr�sh ìpwc k�name parap�nw.

IsodÔnama: mia fr�sh eÐnai èna sÔnolo lektik¸n.


&

$

%

Qr sh tou Kanìna thc An�lushc

O kanìnac thc an�lushc qrhsimopoieÐtai gia na deÐxoume ìti ènasÔnolo fr�sewn S eÐnai mh ikanopoi simo.

Autì apodeknÔetai an me th qr sh tou kanìna thc an�lushcft�soume se antÐfash, dhlad se dÔo lektik� pou to èna eÐnai h�rnhsh tou �llou. An efarmìsoume an�lush se aut� ta lektik�,ft�noume sthn ken fr�sh.


&

$

%

Qr sh tou Kanìna thc An�lushc

O kanìnac thc an�lushc mporeÐ epÐshc na qrhsimopoihjeÐ ìtanjèloume na deÐxoume ìti KB |= φ gia mia b�sh gn¸shc KB kaiprìtash φ.

IsodÔnama: mporoÔme na deÐxoume ìti h prìtash KB ∧ ¬φ eÐnai mhikanopoi simh qrhsimopoi¸ntac an�lush.


&

$

%

Par�deigma

DÐnontai oi ex c prot�seic sta Ellhnik�:

An o monìkeroc eÐnai mujikìc tìte eÐnai aj�natoc, all� an den eÐnaimujikìc tìte eÐnai jnhtì jhlastikì. An o monìkeroc eÐnai jnhtìjhlastikì aj�natoc tìte eÐnai kerasfìroc. An o monìkeroc eÐnaikerasfìroc tìte eÐnai magikìc.

Na deÐxete: O monìkeroc eÐnai magikìc.


&

$

%

To Par�deigma se Protasiak Logik

Ja qrhsimopoi soume ta ex c protasiak� sÔmbola:

• Mythical, ja parist�nei thn prìtash: o monìkeroc eÐnaimujikìc.

• Mortal, ja parist�nei thn prìtash: o monìkeroc eÐnai jnhtìc.

• Mammal, ja parist�nei thn prìtash: o monìkeroc eÐnaijhlastikì.

• Horned, ja parist�nei thn prìtash: o monìkeroc eÐnaikerasfìroc.

• Magical, ja parist�nei thn prìtash: o monìkeroc eÐnai magikìc.


&

$

%

To Par�deigma se Protasiak Logik

Oi dosmènec prot�seic parist�nontai se protasiak logik wc ex c:

Mythical ⇒ ¬Mortal

¬Mythical ⇒ Mortal

¬Mythical ⇒ Mammal

¬Mortal ∨Mammal ⇒ Horned

Horned ⇒ Magical

'Eqoume na apodeÐxoume thn prìtash Magical.


&

$

%

Suzeuktik Kanonik Morf

Metatrèpoume tic dosmènec prot�seic kai thn �rnhsh thc prìtashcpou èqoume na apodeÐxoume se CNF:

¬Mythical ∨ ¬Mortal

Mythical ∨Mortal

Mythical ∨Mammal

Mortal ∨Horned

¬Mammal ∨Horned

¬Horned ∨Magical

¬Magical


&

$

%

An�lush

Apì thn prìtash ¬Mythical ∨ ¬Mortal kai thnMythical ∨Mammal, èqoume thn ¬Mortal ∨Mammal.

Apì thn prìtash ¬Mortal ∨Mammal kai thn Mortal ∨Horned,èqoume thn Mammal ∨Horned.

Apì thn prìtash Mammal ∨Horned kai thn¬Mammal ∨Horned, èqoume thn Horned.

Apì thn prìtash Horned kai thn ¬Horned ∨Magical, èqoume thnMagical.

Apì ta lektik� M kai ¬M , èqoume thn ken fr�sh (antÐfash).


&

$

%

Orjìthta kai Plhrìthta tou Kanìna thc An�lushc

Orjìthta. 'Estw h b�sh gn¸shc KB. An h φ mporeÐ na apodeiqjeÐ apìthn KB qrhsimopoi¸ntac an�lush, tìte KB |= φ.

Plhrìthta Di�yeushc. An èna sÔnolo fr�sewn KB eÐnai mhikanopoi simo, tìte up�rqei mia apìdeixh thc ken c fr�shc apì thn KB

qrhsimopoi¸ntac an�lush.

ShmeÐwsh: Thn apìdeixh aut mporeÐ na th breÐ opoiosd pote pl rhcalgìrijmoc anaz thshc pou qrhsimopoieÐ ton kanìna thc an�lushc.


&

$

%

Ikanopoihsimìthta kai CSPs

To prìblhma thc ikanopoihsimìthtac gia thn protasiak logik eÐnai jemeli¸dec. 'Opwc eÐdame parap�nw, ta probl mata thclogik c k�luyhc kai thc egkurìthtac mporoÔn na anadiatupwjoÔnwc probl mata ikanopoihsimìthtac.

To prìblhma thc ikanopoihsimìthtac gia thn protasiak logik mporeÐ na diatupwjeÐ wc prìblhma ikanopoÐhshc periorism¸n(CSP). Poiec eÐnai oi metablhtèc, ta pedÐa kai oi periorismoÐ?


&

$

%

Poluplokìthta Ikanopoihsimìthtac

Je¸rhma. To prìblhma tou na apofanjoÔme an mia prìtash thcprotasiak c logik c eÐnai ikanopoi simh ìqi eÐnai NP-complete(Cook, 1971).

Pìrisma. To prìblhma tou na apofanjoÔme an mia prìtash thcprotasiak c logik c eÐnai ègkurh ìqi eÐnai co-NP-complete.

Sunep¸c oi pijanìthtec na brejoÔn algìrijmoi poluwnumikoÔqrìnou gia thn epÐlush twn parap�nw problhm�twn eÐnai polÔmikrèc. 'Omwc up�rqoun apodotikoÐ algìrijmoi gia to prìblhmathc ikanopoihsimìthtac (deÐte gia par�deigma touc algìrijmoucDPLL kai WalkSat apì to biblÐo AIMA).


&

$

%

Fr�seic Horn

Orismìc. Mia fr�sh Horn eÐnai mia fr�sh pou èqei to polÔ ènajetikì lektikì.

Dhlad , mia fr�sh Horn apant�tai stic ex c morfèc:

Q

¬P1 ∨ ¬P2 ∨ . . . ∨ ¬Pn ∨Q (isodÔnama: P1 ∧ P2 ∧ . . . ∧ Pn ⇒ Q)

¬P1 ∨ ¬P2 ∨ . . . ∨ ¬Pn

ìpou P1, . . . , Pn, Q eÐnai protasiak� sÔmbola.

Je¸rhma. An h φ eÐnai sÔzeuxh fr�sewn Horn tìte hikanopoihsimìthta thc φ mporeÐ na apofasisteÐ se poluwnumikìqrìno.


&

$

%

AnakefalaÐwsh

'Estw KB èna sÔnolo prot�sewn thc protasiak c logik c kai φ

mia prìtash thc protasiak c logik c. Pwc mporoÔme naapofasÐsoume an KB |= φ?

• MporoÔme na qrhsimopoi soume touc shmasiologikoÔc orismoÔcpou d¸same, kai na k�noume th sqetik apìdeixh.

• MporoÔme na qrhsimopoi soume pÐnakec alhjeÐac.

• MporoÔme na efarmìsoume touc kanìnec sumperasmoÔ poud¸same parap�nw (p.q., an�lush).

• MporoÔme na qrhsimopoi soume touc apodotikoÔcalgìrijmouc ikanopoihsimìthtac DPLL WalkSat

(Kef�laio 7.6 tou biblÐou AIMA).


&

$

%

AdunamÐec thc Protasiak Logik c

JewreÐste ton ex c kanìna gia ton kìsmo tou Wumpus:

An s' èna tetragwn�ki de gÐnetai antilhpt murwdi� tìteoÔte sto Ðdio to tetragwn�ki oÔte se geitonikì tou denmporeÐ na eÐnai o Wumpus.

P¸c mporoÔme na anaparast soume autìn ton kanìna seprotasiak logik ?

Prèpei na gr�youme ènan kanìna gia k�je sqetikìtetragwn�ki! Gia par�deigma:

¬S11 ⇒ ¬W11 ∧ ¬W12 ∧ ¬W21


&

$

%

AdunamÐec thc Protasiak Logik c

• Den up�rqei trìpoc sthn protasiak logik na ekfr�soumek�ti gia ìla ta antikeÐmena enìc sugkekrimènou eÐdouc (p.q., giak�je tetragwn�ki).

• Den up�rqei trìpoc na mil soume gia èna sugkekrimènoantikeÐmeno, tic idiìthtec tou kai tic sqèseic tou me �llaantikeÐmena.

• Den up�rqei trìpoc na mil soume gia thn Ôparxh ( thn mhÔparxh) enìc antikeimènou me sugkekrimènec idiìthtec.

Mhn anhsuqeÐte! Aut� mporoÔme na ta ekfr�soume sthn logik pr¸thc t�xhc.


&

$

%

Pr�ktorac Basismènoc sth Gn¸sh

function Propositional-KB-Agent(percept) returns an action

static KB, b�sh gn¸shct, metrht c gia to qrìno, arqik� 0

Tell(KB,Make-Percept-Sentence(percept, t))for each action in the list of possible actions do

if Ask(KB,Make-Action-Query(t, action)) thenTell(KB,Make-Action-Sentence(action, t))t ← t + 1return action

end


&

$

%

Anagn¸smata

Kef�laio 7 apì to biblÐo AIMA: LogikoÐ Pr�ktorec (Enìthtec 7.1èwc 7.5 kai 7.7).

Pr ktorecBasismènoisth Gn¸sh - UoAcgi.di.uoa.gr/~ys02/dialekseis2011/propositional2spp.pdf ·...

Documents

Transcript of Pr ktorecBasismènoisth Gn¸sh - UoAcgi.di.uoa.gr/~ys02/dialekseis2011/propositional2spp.pdf ·...