TL;DR
1์ฐจ ๋ ผ๋ฆฌ(FOL)๋ ๊ฐ์ฒด์ ๋ํ ์ง์ ์ ์์ยท๋ณ์ยท์ ์ดยท์ํ์ฌ๋ก ๊ตฌ์กฐํํ์ฌ, ์์ฑยท๊ด๊ณยท์ผ๋ฐ ๊ท์น์ ํ์์ ์ผ๋ก ํํํ๊ณ ์ถ๋ก ํ ์ ์๊ฒ ํ๋ ๋ ผ๋ฆฌ ์ฒด๊ณ์ด๋ค.
๐ง 1์ฐจ ๋ ผ๋ฆฌ (First-Order Logic, FOL)
1. ๋ช ์ ๋ ผ๋ฆฌ(Propositional Logic)์ ํ๊ณ
๋ช ์ ๋ ผ๋ฆฌ๋ ๋ฌธ์ฅ ์ ์ฒด๋ฅผ ํ๋์ ์ฐธยท๊ฑฐ์ง ๋จ์๋ก ๋ค๋ฃจ๊ธฐ ๋๋ฌธ์ ๋ฌธ์ฅ ๋ด๋ถ์ ์ธ๋ถ ๊ตฌ์กฐ๋ฅผ ๋๋ฌ๋ด์ง ๋ชปํ๋ค.
- ์์:
- : โ์ํฌ๋ผํ ์ค๋ ์ฌ๋์ด๋คโ
- : โ๋ชจ๋ ์ฌ๋์ ์ฃฝ๋๋คโ
- ํ๊ณ:
"์ํฌ๋ผํ ์ค","์ฌ๋","์ฃฝ๋๋ค"๊ฐ์ ๊ฐ๋ณ ๊ตฌ์ฑ ์์๋ฅผ ๋ถ๋ฆฌํด ๋ค๋ฃจ๊ฑฐ๋,"๋ชจ๋ ","์ด๋ค"๊ฐ์ ์ํ์ ์ผ๋ฐ ๊ท์น์ ์ง์ ํํํ๊ธฐ ์ด๋ ต๋ค. ์ฆ, ์ถ๋ก ์ ์ฌ๋ฃ๊ฐ ๋๋ ๊ฐ์ฒด์ ๊ด๊ณ๋ฅผ ๊ตฌ์กฐ์ ์ผ๋ก ๊ธฐ์ ํ๋ ๋ฐ ํ๊ณ๊ฐ ์๋ค.
2. 1์ฐจ ๋ ผ๋ฆฌ(First-Order Logic)์ ํต์ฌ ์์
1์ฐจ ๋ ผ๋ฆฌ๋ ๋ช ์ ๋ณด๋ค ๋ ์์ ๊ตฌ์กฐ ๋จ์๋ก ์ง์์ ํํํจ์ผ๋ก์จ ๊ฐ๋ณ ๋์๊ณผ ๊ทธ๋ค ์ฌ์ด์ ๊ด๊ณ, ์ผ๋ฐ ๊ท์น์ ํ์์ ์ผ๋ก ๊ธฐ์ ํ๋ค.
-
ํญ (Terms): ๋์์ ๊ฐ๋ฆฌํค๋ ํํ
- ์์ (Constants): ํน์ ํ ๊ฐ์ฒด (์:
Socrates,Naver) - ๋ณ์ (Variables): ์์์ ๊ฐ์ฒด (์:
x,y) - ํจ์ (Functions): ๊ฐ์ฒด๋ฅผ ๋ค๋ฅธ ๊ฐ์ฒด์ ๋์์ํค๋ ํํ (์:
FatherOf(x))
- ์์ (Constants): ํน์ ํ ๊ฐ์ฒด (์:
-
์ ์ด (Predicates): ๋์์ ์์ฑ์ด๋ ๋์๋ค ์ฌ์ด์ ๊ด๊ณ
- : ๋ ์ฌ๋์ด๋ค.
- : ๋ ๋ฅผ ์ข์ํ๋ค.
-
๋ ผ๋ฆฌ ์ฐ๊ฒฐ์ฌ (Connectives): ์ฌ๋ฌ ๋ช ์ ๋ฅผ ๊ฒฐํฉ (AND: , OR: , NOT: , IF-THEN: )
-
์ํ์ฌ (Quantifiers): ๋ณ์๊ฐ ๊ฐ๋ฆฌํค๋ ๋ฒ์๋ฅผ ์ง์
- ๋ณดํธ ์ํ์ฌ (): ๋ชจ๋ ์ ๋ํ์ฌ (์: )
- ์กด์ฌ ์ํ์ฌ (): ์ด๋ค ๊ฐ ์กด์ฌํ๋ค (์: )
3. ์ถ๋ก ์ ์์ (์ผ๋จ๋ ผ๋ฒ์ ์์ํ)
1์ฐจ ๋ ผ๋ฆฌ๋ ๊ฐ๋ณ ์ฌ์ค๊ณผ ์ผ๋ฐ ๊ท์น์ ํ๋์ ํ์ ์ฒด๊ณ ์์์ ์ฐ๊ฒฐํ์ฌ ์๋ก์ด ๊ฒฐ๋ก ์ ๋์ถํ๊ฒ ํด์ค๋ค.
- ์ผ๋ฐ ๊ท์น: (๋ชจ๋ ์ฌ๋์ ์ฃฝ๋๋ค)
- ๊ฐ๋ณ ์ฌ์ค: (์ํฌ๋ผํ ์ค๋ ์ฌ๋์ด๋ค)
- ํ์์ ์ถ๋ก : (๋ฐ๋ผ์ ์ํฌ๋ผํ ์ค๋ ์ฃฝ๋๋ค)
์ด์ฒ๋ผ 1์ฐจ ๋ ผ๋ฆฌ๋ ๊ฐ๋ณ ์ฌ์ค๊ณผ ์ผ๋ฐ ๊ท์น์ ์ฐ๊ฒฐํ์ฌ ๋ ผ๋ฆฌ์ ๊ฒฐ๋ก ์ ๋์ถํ ์ ์๋ ๊ตฌ์กฐ๋ฅผ ์ ๊ณตํ๋ค.
4. 1์ฐจ ๋ ผ๋ฆฌ์ ์๋ฏธ
1์ฐจ ๋ ผ๋ฆฌ์ ํต์ฌ ๊ฐ์น๋ ์์ฐ์ด ์์ ๋ชจํธํ ์๋ฏธ๋ฅผ ๊ฐ์ฒด, ์์ฑ, ๊ด๊ณ, ๊ท์น์ผ๋ก ๋ถํดํ์ฌ ํ์ ์ธ์ด๋ก ์ฎ๊ธฐ๋ ๋ฐ ์๋ค. ์ด๋ ๋จ์ํ ๋ฌธ์ฅ์ ๋ณต์กํ๊ฒ ๋ง๋๋ ๊ฒ์ด ์๋๋ผ, ์ง์์ ๊ตฌ์กฐ์ ์ผ๋ก ํํํ๊ณ ์ถ๋ก ๊ฐ๋ฅํ๊ฒ ๋ง๋ ๋ค ๋ ๋ฐ ์๋ค.
Discussion
Comments
๋๊ธ์ ์น์ธ ํ ๊ณต๊ฐ๋ฉ๋๋ค.