1. Propositional Logic (๋ช ์ ๋ ผ๋ฆฌํ)
1) Example
์ด๋ฒ ๋จ์ ๋ด๋ด ์ง๊ฒน๋๋ก ๋ณด๊ฒ ๋ Wumpus World game์ด๋ค. ์ด ๊ฒ์์ (1,1)์์ ์ฉ์ฌ๊ฐ ์ถ๋ฐํด ๊ดด๋ฌผ๊ณผ ํจ์ ์ ํผํด gold๋ฅผ ๋ฌด์ฌํ ์ฐพ๋ ๊ฒ์ด ๋ชฉํ์ด๋ค. ํจ์ ์ด ์์ผ๋ฉด ํจ์ ์ ์ฌ๋ฐฉ์ผ๋ก breeze ๋ฐ๋์ด ๋ถ๊ณ , ๊ดด๋ฌผ์ด ์์ผ๋ฉด ๊ดด๋ฌผ์ ์ฌ๋ฐฉ์ผ๋ก ์ ์ทจ strench๊ฐ ํ๊ธด๋ค. ์ด ํํธ๋ฅผ ์ด์ฉํด ์ต์ํ์ผ๋ก ์์ง์ฌ ๋ฌด์ฌํ gold๋ฅผ ์ฐพ์ผ๋ฉด ๋๋ค. ์ฉ์ฌ๊ฐ ์ด๋ค Action์ ์ทจํ ๋๋ง๋ค cost๊ฐ ๋ ๋ค.
์ด๊ฑด ์์๋ ๋๊ณ ๋ชฐ๋ผ๋ ๋๋๋ฐ ์ฉ์ฌ๋ ํ์ด์ ์ ์ ์๋ค. ํ์ด์ ์๋ฉด ์ง์ ๋ฐฉํฅ์ผ๋ก ์ญ ๋ ์๊ฐ๋๋ฐ, ๊ดด๋ฌผ์ด ๋ง์ผ๋ฉด ์๋ฆฌ๋ฅผ ์ง๋ฅด๋ฉด์ ์ฃฝ๋๋ค. ์ด ์๋ฆฌ๋ฅผ ๋ฃ๊ณ ๊ดด๋ฌผ์ ์์น๋ฅผ ์์ธกํ ์ ์๋ค.
์ฉ์ฌ๋ ์๊ธฐ๊ฐ ์๋ ์นธ์์ ์ ๋ณด๋ฅผ ์์งํ๋ค. ์ด ์นธ์ ๋ฐ๋์ด ๋ถ๋์ง, ์ ์ทจ๊ฐ ๋๋์ง, ๊ธ์ด ์๋์ง, ๊ดด๋ฌผ์ด ์ฃฝ๋ ์๋ฆฌ๋ฅผ ๋ค์๋์ง, ์ด๋๋ก ์์ง์ผ ์ ์๋์ง. ์ฆ Partialy observableํ ์ํฉ์ด๋ค.
1,1 ์์ ์ฉ์ฌ๋ ์ ์ทจ์ ๋ฐ๋์ด ๋ถ์ง ์์์ ํ์ธํ๋ค. ๋ฐ๋ผ์ 1,2 ์ 2,1 ์ ์์ ํ๋ค.
2,1๋ก ์์ง์๋๋ ๋ฐ๋์ด ๋ถ๋ค. ๋ฐ๋ผ์ 2,2 ๋๋ 3,1์ ํจ์ ์ด ์๋ค. 1,1๊ณผ 1,2๋ ์์ ํ๋ค๋๊ฒ ํ์ธ ๋์์ผ๋ 1,2๋ก ์์ง์ธ๋ค.
1,2 ๋ก ์์ง์๋๋ ์ ์ทจ๊ฐ ๋๋ค. ์ผ๋จ ๋ฐ๋์ ์๋ถ์์ผ๋ 2,2๋ ์์ ํ๋ค. ๊ทธ๋ฌ๋ฏ๋ก 3,1์ ํจ์ ์ด, 1,3์ ๊ดด๋ฌผ์ด ์๋ค. 2,2๋ก ์ด๋ํ๋ค.
2,2์๋ ์๋ฌด๊ฒ๋ ์์ผ๋ฏ๋ก 2,3์ด ์์ ํ๋ค. ์์ง์๋๋ ๊ธ์ด ์์๋ค. ์ด์ ๋ฐฉ๋ฌธํ๋ ๊ณณ์ ๋ฐ๋ผ ๋ค์ 1,1๋ก ๋์์ค๋ฉด ๋๋ค. ์ด์ ์ด๊ฑธ PL์ ์ด์ฉํด CSP๋ฌธ์ ์ฒ๋ผ ํ์ด๋ด๋ณด์.
2) Syntax
- atomic sentences : single proposition symbol. ํ๋์ ๋ช ์ ๊ธฐํธ. P, Q, R๊ณผ ๊ฐ์ ๋ณ์๋ True, False ๋ฑ.
- Complex sentences : atomic sentence๋ค์ด ๋ ผ๋ฆฌ๊ธฐํธ๋ก ์ฐ๊ฒฐ๋ ๋ฌธ์ฅ.
(๏ฟข : not(nagative), ∧ : and(conjunction), ∨ : or(disconjunction), ⇒ : implies, ⇔: if and only if)
- literal : atomic sentence(=positive literal) ๊ณผ nagated atomic sentence( = nagative literal)๋ก ์ด๋ฃจ์ด์ง.
์ฆ, ๋ช ์ ๊ธฐํธ ๋ธ๋ ํ๋ ์๊ฑฐ๋, ๋ช ์ ๊ธฐํธ์ not ๊ธฐํธ ํ๋ ๋ถ์ด ์๋ ์ ๋ค์ด literal
3) Semantics
- ํ์ค์ ์ธ logic์์ ๋ชจ๋ ๋ฌธ์ฅ์ true ๋๋ false๋ผ๋ ๊ฐ์ ๊ฐ์ง๊ฒ ๋๋ค. ์ฐ๋ฆฌ๋ ๊ฐ๋ฅํ ์ธ๊ณ๋ฅผ model์ด๋ผ๋ ๊ฐ๋ ์ผ๋ก ๋ํ๋ธ๋ค. ๊ฐ literal์ด ์ด๋ค ๊ฐ์ ๊ฐ์ง๋์ ๋ฐ๋ผ์ ๋ฌธ์ฅ ์ ์ฒด์ ์ง๋ฆฌ๊ฐ์ด ๋ฌ๋ผ์ง๊ธฐ ๋๋ฌธ์ literal์ ํ ๋นํ๋ ์ง๋ฆฌ๊ฐ ํ๋ํ๋์ ๋ฐ๋ผ ๊ฐ๋ฅํ possible world๊ฐ ๋ฌ๋ผ์ง๋๋ฐ, ๊ฐ๊ฐ์ ๊ฒฝ์ฐ๋ค์ model์ด๋ผ๊ณ ๋ถ๋ฅธ๋ค.
- semantics (์๋ฏธ๋ก ) ์ ์ด๋ค ๋ชจ๋ธ์์ ๋ฌธ์ฅ์ ์ง์ ์ฌ๋ถ๋ฅผ ๊ฒฐ์ ํ๊ธฐ ์ํ ๊ท์น์ ์ ์ํ๋ค.
PL์์์ semantic์ ์ด๋ค model์ด ์ฃผ์ด์ก์ ๋ ๊ทธ sentence์ ์ฐธ ๊ฑฐ์ง ๊ฐ์ ๊ณ์ฐํ๋ ๋ฐฉ๋ฒ, ์ผ์ข ์ ๊ท์น์ ๋ชจ์๋ ๊ฒ์ ๋งํ๋ค.
์ ํ์์ ๊ฐ๊ฐ ํ ํ์ด ํ๋์ model์ด๋ค.
โ sentence ๋ knowledge representation language๋ผ๊ณ ๋ถ๋ฆฌ๋ ์ธ์ด๋ก ํํ๋๋ค.
โก axiom : ๊ณต๋ฆฌ ๋ ๋ค๋ฅธ ๋ฌธ์ฅ์ผ๋ก ๋ถํฐ ์ฆ๋ช ๋์ง ์์๋, ๊ทธ ๋ฌธ์ฅ ์์ฒด๋ก true๋ผ๊ณ ๊ฐ์ฃผํ๋ค.
โข ๋ฌธ์ฅ๋ค์ representation language์ syntax(๋ฌธ๋ฒ)์ ๋ง๊ฒ ํํ๋๋ค. ๊ทธ๋ฆฌ๊ณ ์ด๊ฒ์ well-formed sentence๋ฅผ ํน์ ํ๋ค.
โฃ logic์ ๋ฐ๋์ semantic ๋๋ ๋ฌธ์ฅ์ ์๋ฏธ๊ฐ ์ ์๋์ด์ผ ํ๋ค. semantic์ ๋ฌธ์ฅ์ด ๊ฐ ๊ฐ๋ฅ์ธ๊ณ์ ๋ํด์ true์ธ์ง false์ธ์ง๋ฅผ ์ ์ํ๋ค.
โค knowledge base(KB: ์ง์์ฒด๊ณ)๋ ๋ฌธ์ฅ๋ค์ ์งํฉ์ด๋ค. ์ด KB๋ ์ฒ์์๋ background knowledge๋ก ์์ํด์ ์ถ๋ก ์ ํตํด ๋ฌธ์ฅ์ ์ถ๊ฐํด๋๊ฐ๋ค.
4) Example
์์ ์ดํด๋ดค๋ Wumpus World๋ฅผ ๋ ์ฌ๋ ค๋ณด์. ์ฌ๊ธฐ์ ํจ์ ์ ๋ํด KB๋ฅผ ๋ง๋ค์ด๋ณด์.
๋จผ์ ๊ธฐ๋ณธ์ ์ธ ๊ท์น(๊ณต๋ฆฌ)๋ฅผ ์ค์ ํด์ฃผ์
- ์์์ง์ ์๋ ํจ์ ์ด ์์ผ๋ฉด ์๋๋ค (R1) : ๏ฟขP(1,1)
- (1,1)์์ ๋ฐ๋์ด ๋ถ๋ฉด (2,1) ๋๋ (1,2)์ ํจ์ ์ด ์๋ค (R2) : B(1,1) ⇔ (P(1,2) ∧ P(2,1))
.
.
.
๊ทธ๋ฆฌ๊ณ ๊ด์ธก ๊ฒฐ๊ณผ
- (1,1)์์๋ ๋ฐ๋์ด ๋ถ์ง ์๋๋ค (R4) : ๏ฟขB(1,1)
- (2,1)์์๋ ๋ฐ๋์ด ๋ถ๋ค (R5) : B(2,1)
์ด๋ฌํ ์๋ ค์ง ์ฌ์ค์ ๋ฐํ์ผ๋ก truth table์ ๋ง๋ค์ด๋ณด์.
R๋ค์ ์ด๋ฏธ ์๋ ค์ง ์ฌ์ค๋ก, ์๋ค๋ true์ฌ์ผ๋ง ํ๋ค. ์ฆ, ๊ด์ธก ๊ฒฐ๊ณผ๋ฅผ ๋ฐํ์ผ๋ก ์ถ๋ก ํ ์ ๋ค์ด R, ์ฆ knowledge base๋ฅผ ์ฐธ์ผ๋ก ๋ง๋๋ ๋ฌธ์ฅ์ด ์๋ก์ด ์ฐธ์ธ ๋ฌธ์ฅ์ด๋ค.
์ง๊ธ ์ฐ๋ฆฌ๋ (1,1)~(3,1)์ ๋ํ ์ ๋ณด๋ฅผ ์๊ณ ์๋ค. ์ด ์ ๋ณด๊ฐ R1~R5 ์์ ๋ด๊ฒจ ์๋ค. ์ด ์์ด๋ค์ด KB์ด๋ค.
๊ทธ๋ฆฌ๊ณ ์ฐ๋ฆฌ๋ (1,1)~(3,1)์์ ๊ฐ๋ฅํ ๋ชจ๋ ๊ฒฝ์ฐ์ ์๋ฅผ ์ ์ด๋ณด์๋ค. 2์ 7์ ๊ณฑ, ์ด 128๊ฐ์ ๊ฒฝ์ฐ์ ์๊ฐ ์๋ค. ์ด ์๋ง์ ๊ฒฝ์ฐ์ ์์์ KB๋ฅผ true๋ก ๋ง๋๋ ๊ฒฝ์ฐ, ๊ทธ model์ ๋ฐํ์ผ๋ก ์๋ก์ด KB๋ฅผ ๋ง๋ค์ด ๋ผ ์ ์๋ค.
5) Entailment and Inference
โ ๋ง์ฝ sentence α๊ฐ model m์์ true์ผ ๋, m satisfie α ๋๋ m is a model of α๋ผ๊ณ ๋งํ๋ค. α์ model๋ค์ ์งํฉ, ์ฆ α์ ๋ชจ๋ ๋ชจ๋ธ๋ค, α๊ฐ true์ธ ํ ์ด๋ธ์ ๋ชจ๋ ํ๋ค์ M(α)๋ผ๊ณ ํํํ๋ค.
โก ๋ง์ฝ sentence α ๊ฐ sentence β ๋ฅผ entailํ ๋, α โจ β ๋ผ๊ณ ํํํ๋ค.
๋ชจ๋ model์์ α๊ฐ true๋ผ๋ฉด β ์ญ์๋ true์ด๋ค.
โข Inference(์ถ๋ก )์ ์ด๋ค old sentence๋ก๋ถํฐ new sentence๊ฐ ๋์ถ๋์์ ๋๋ฅผ ๋งํ๋ค. ๋ง์ฝ inference algorithm i๊ฐ KB๋ก๋ถํฐ α๋ฅผ ๋์ถํด๋๋ค๋ฉด, KB โขi α๋ผ๊ณ ์ธ ์ ์์ผ๋ฉฐ , "α๋ i์ ์ํด KB๋ก๋ถํฐ derive๋์๋ค" ๋๋ "i derives α from KB" ๋ผ๊ณ ๋งํ ์ ์๋ค.
โฃ inference algorithm์ด true์ธ ๋ฌธ์ฅ๋ง deriveํ์ฌ entail๋ ์ ์๋ ๋ฌธ์ฅ๋ง entail์ํค๋ฉด, soundํ๋ค๊ณ ๋งํ๊ณ , ๋์ฌ ์ ์๋ ๋ชจ๋ true์ธ sentence๋ฅผ ๋์ถํด๋ด entailํ ์ ์๋ ๋ชจ๋ ๋ฌธ์ฅ์ ์ฐพ์ ์ ์์ผ๋ฉด completeํ๋ค๊ณ ๋งํ๋ค.
์ฆ soundํ ๊ฒฝ์ฐ ๋ชจ๋ entailํ๋ sentence๋ฅผ ๋ค ์ฐพ๋ ๊ฑด ์๋์ง๋ง ์ฐพ์ sentence๋ ๋ค entail ํ ์ ์๋ ๊ฒ์ด๊ณ , completeํ ๊ฒฝ์ฐ ๋ชจ๋ entail ํ ์ ์๋ sentence๋ฅผ ๋ค ์ฐพ์ ๊ฑฐ์ง๋ง, ์๋๋ sentence๋ ์์ฌ์์ ์ ์๋ค.
(a) (1, 2)์๋ ํจ์ ์ด ์๋ค๋ ์๋ก์ด α1 ์ ๋์ถํด๋๋ค๊ณ ์น์. KB๊ฐ true์ธ ๋ชจ๋ model์์ α1 ์ญ์ true์ด๋ฏ๋ก KB๋ a๋ฅผ entail ํ๋ค๊ณ ๋ณผ ์ ์๋ค.
(b) (2, 2)์๋ ํจ์ ์ด ์๋ค๋ α2๋ฅผ ๋์ถํด ๋๋ค๊ณ ์น์. ์ด๋ KB๊ฐ true์ธ ๋ชจ๋ model์์ ๋ง์กฑํ๋ ๊ฒ์ด ์๋๊ธฐ ๋๋ฌธ์ ๋ฌด์กฐ๊ฑด ํจ์ ์ด ์๋ค๊ณ ํ ์๋ ์๋ ๊ฒ์ด๋ค. ์ฆ, Entailํ์ง ์๋ค.
2. Model Cheking Approach
- KB๊ฐ α๋ฅผ entail ํ๋์ง ์ํ๋์ง๋ฅผ ๊ฒฐ์ ํ๊ธฐ ์ํด์๋ model checking์ ํด์ α๊ฐ KB๊ฐ TRUE์ธ ๋ชจ๋ model์์ true์ธ์ง ํ์ธํด์ผ ํ๋ค.
P,Q,R์ด๋ผ๋ ์ธ๊ฐ์ symbol์ด ์์ ๋ 2^3๊ฐ์ truth table์ด ๋ง๋ค์ด์ง ์ ์๋ค. ์ด truth table์์ KB๊ฐ true๊ฐ ๋๋ model์ด ์์ ๋, ๊ทธ model ๋ชจ๋์์ α๊ฐ true์ฌ์ผ์ง๋ง KB๊ฐ α๋ฅผ entailํ๋ค๊ณ ํ ์์๋ค.
์๊ณ ๋ฆฌ์ฆ์ ๋ค์๊ณผ ๊ฐ๋ค.
KB๊ฐ α๋ฅผ entailํ๋์ง๋ฅผ ์์๋ณด๋ ํจ์ TT-ENTAILS?ํจ์๋ฅผ ๋ณด์.
KB์ α์ ์กด์ฌํ๋ ๋ชจ๋ Proposition symbol๋ค, ๋ชจ๋ literal๋ค์ symbols๋ผ๋ ๋ฆฌ์คํธ์ ๋ด๊ณ , TT-CHECK-ALLํจ์๋ฅผ ํธ์ถํ๋ค.
TT-CHECK-ALL ํจ์๋ symbol ํ๋ํ๋์ ์ง๋ฆฌ๊ฐ์ ๋ฃ์ด์ model์ ๋ง๋ค๊ณ ํ์์ ์งํํ๋ค.
์ฐ์ symbols์ด ๋น์ด์๋ค๋ฉด, model์ด KB๋ฅผ ๋ง์กฑํ๋์ง, ์ฆ model์ด KB๊ฐ true์ธ์ง๋ฅผ ํ๋ณํด๋ณธ๋ค. ๋ง์ฝ ํด๋น model์์ KB๊ฐ true๋ผ๋ฉด, α ๋ํ ๊ทธ model์์ true์ฌ์ผ ํ๋ค. ๊ทธ๋์ true๋ฉด true๋ฅผ, false๋ฉด false๋ฅผ returnํ๋ค.
๋ง์ฝ model์์ KB๊ฐ ์ ์ด์ false๋ผ๋ฉด ๋ณผ ํ์๊ฐ ์์ผ๋ฏ๋ก ๊ทธ๋ฅ true๋ฅผ ๋ฐํํด์ค๋ค.
๋ง์ฝ symbols์ด ๋น์ด์์ง ์๋ค๋ฉด, P์ ์ฒซ๋ฒ์งธ symbol์, rest์ ๋๋จธ์ง symbol์ ๋ฃ์ด์ค๋ค.
๊ทธ๋ฆฌ๊ณ ๋จผ์ TT-CHECK-ALLํจ์๋ฅผ P=true์ผ๋์ P=false์ผ ๋ ๊ฐ๊ฐ ํธ์ถํด์ and ์ฐ์ฐ์ ์์ผ์ค๋ค.
์ด ๊ณผ์ ์ ์ฝ๊ฒ ๋งํด์ model์ ๋ง๋ค์ด์ฃผ๋ ๊ณผ์ ์ด๋ผ๊ณ ์๊ฐํ๋ฉด ๋๋ค. model์์ False๊ฐ ํ๋๋ผ๋ ๋ฐํ๋๋ ์๊ฐ, KB๋ true์ด์ง๋ง α๋ false์ธ model์ด ์์๋ค๋ ๊ฒ์ด๊ธฐ ๋๋ฌธ์ entailํ ์ ์๋ค.
* Analysis of Model Checking Approach
- ์ด ์๊ณ ๋ฆฌ์ฆ์ entailment์ ์ ์๋ฅผ ์ง์ ์ ์ผ๋ก ํ์ฉํ ๊ฒ์ด๊ธฐ ๋๋ฌธ์ ๋น์ฐํ๋ soundํ๋ค.
- ๋ํ ๋ชจ๋ KB์ α์ ๋ํด ์ํ๋๊ณ , ํญ์ ๋๊น์ง ์ฐพ๊ธฐ ๋๋ฌธ์(=DFS) Complete ํ๊ธฐ๋ ํ๋ค.
- Time Complexity : O(2^n) // ๋ชจ๋ model์ ์ฐพ๋ ๊ฒฝ์ฐ์ ์ = 2x2x...x2 (n๊ฐ) , n์ symbol ๊ฐ์
Space Complexity : O(n) // ํ ๋ฒ์ ๋ชจ๋ธ ํ๋์ฉ ๊ฒ์ฌํ๋๊น ํ ๋ฒ์ ์ต๋ n
'๐ก๐ธ๐ธ๐ถ5: ๐ฆ๐๐๐๐ถ ๐ฐ๐๐พ๐ > Artificial Intelligence(COSE361)' ์นดํ ๊ณ ๋ฆฌ์ ๋ค๋ฅธ ๊ธ
[์ธ๊ณต์ง๋ฅ] 7. Propositional Logic - 3 (2) | 2021.04.25 |
---|---|
[์ธ๊ณต์ง๋ฅ] 7. Propositional logic - 2 (1) | 2021.04.25 |
[์ธ๊ณต์ง๋ฅ] 6. Constraint Satisfaction Problems (0) | 2021.04.24 |
[์ธ๊ณต์ง๋ฅ] 5. Adversarial Search(์ ๋์ ํ์) (0) | 2021.04.24 |
[์ธ๊ณต์ง๋ฅ] 4. Beyond Classical Search - 2 (0) | 2021.04.24 |