[AI] Knowledge Representation

1. Propositional logic
 - 명제 논리
 - 서술문으로서 그 내용에 대해 참이나 거짓을 담고 있는 문장

2. Predicate logic
 - 술어 논리
 - 명제 논리를 기반으로 기호화시켜 관계를 나타낼 수 있고, 기호를 통해 수량도 나타낼 수 있게 한 것

3. Quantifier
 - 정량자, 전체 정량자(∀), 존재 정량자(∃) 두가지가 있다.
 - ∀ : 전체 정량자, '모든'
 - ∃ : 존재 정량자, '일부'

4. First-order logic
 - 일차 술어 계산
 - 술어 계산에서 정량자가 변수에만 적용되고, 술어나 함수에 대해서는 적용되지 않는 경우

5. Conversion to clause form
 1) implication 제거
  ex) p -> q = ￢p ∨ q
 2) 부정의 범위를 줄임
  ex) ￢(∃x)P(x) <=> (∀ㅌ)(￢P(x))
 3) 변수의 변환
  ex) (∀x)[P(x) -> (∃x)Q(x)] <=> (∀x)[P(x) -> (∃y)Q(y)]
 4) 정량자를 제거
  ex) (∀x)[(∃y)P(x, y)] <=> (∀x)P(x,F(x))
 5) prenex form 변환
  ex) (∀x)[P(x) -> (∀y)Q(y)] <=> (∀x)(∀y)[P(x)->Q(y)]
 6) global 정량자 제거
 7) ∧ 제거
 8) 변수 이름 재정의

6. Resolution in Propositional logic
 Given Axioms         Conversion to clause Form
   P                         P
   (P∧Q)->R              ￢P ∨ ￢Q ∨ R
   (S∨T)->Q              ￢S ∨ Q 
   T                         ￢T ∨ Q  
                              T

  To Prove R,
  ￢P ∨ ￢Q ∨ R                   ￢R
            └─────────┘
                      ￢P ∨ ￢Q                      P
                            └─────────┘
                                         ￢Q                     ￢T ∨ Q  
                                           └─────────┘
                                                        ￢T                          T
                                                          └─────────┘ 
                                                                       □        -------------> R 증명 완료

7. The Most General Unifier
 - 술어 논리에서 variable의 value를 최대한 정해주는 집합
 - UNIFY 함수를 호출하면 반환해준다.

8. Procedural Knowledge
 - 사람이 instruction의 순서를 정해준다.

9. Declarative Knowledge
 - 사람이 순서를 정해주지 않아도 컴퓨터가 스스로 순서를 정해서 수행한다.
 - 모든 가짓수를 계산해 맞는 답을 찾음
 - 사람이 instruction의 순서를 정해주는 것은 cost가 크므로 Declarative 방식이 유리할 때가 있다.

10. Closed World Assumption
 - 닫힌 세계이므로 현재 명시된 명제로 추론이 불가능하면 그 명제는 거짓이 된다.

11. Open World Assumption
 - 열린 세계이므로 현재 명시된 명제로 추론이 불가능 하다면 그 명제는 알 수 없는 명제가 된다.