2장. 술어 해석(Predicate Calculus)(2)

[인공지능 2장. 술어 해석(Predicate Calculus)(2)]

[변수와 한정의 영역] 

 : 논리식이 왜 등장하는지, 어디에 쓰이는지 정도만 숙지(변형숙지필요X)

[부정과 한정사와의 관계] #참고만

: ㄱ∃X p(X) = ∀X ㄱp(X)  

: ㄱ∀X p(X) = ∃X ㄱp(X)

[서술 논리의 중요한 특징]

: 서술 논리로 표현된 주어진 사실로부터 기계적, 계산적 조작 과정을 통해 새로운 사실 추론가능한 추론 규칙이 존재한다.

[만족시키다(satisfy)와 논리적 귀결(logically follow)]

- 만족시키다(satisfy) : 어떤 해석 I 하에서 서술 논리식 S가 참이면, 해석 I는 S를 만족(satisfy)시킨다.

- 논리적 귀결(logically follow) : 서술 논리식의 집합 S를 만족시키는 모든 해석이 서술 논리식 X를 만족시키면, X는 S의 논리적 귀결.

   ex) PvQ가 참이 되는 모든 해석에 대해 P도 참. => P는 PvQ의 논리적 귀결

[추론 규칙(inference rules)] #간단한거만

: 주어진 문장의 집합으로부터 기계적, 계산적 과정을 통해 새로운 문장을 도출해 낼수 있는 규칙

<명제 논리>

1) Modus popens : P와 P=>Q 로부터 Q를 추론      ex) P가 true고 P=>Q가 true 면, Q는 true.

2) Modus tollens : P=>Q와 ㄱQ로부터 ㄱP를 추론

3) And elimination : PㅅQ가 참이면 P와 Q도 참

4) And introduction: P와 Q가 참이면 PㅅQ도 참

ex) 모든사람은 죽는다, 소크라테스는 사람이다.  =>  소크라테스는 죽는다.

ex) 가족추론 #생략

ex) 할아버지 추론

  - ∀X∀Y father(X,Y) => parent(X,Y) {abel/X, mary/Y}   #변수삽입

    father(abel, mary) => parent(abel, mary)

  

  - ∀X∀Y∀Z father(X,Y) ㅅ parent(Y,Z) = > grandfather(X,Z)

[논리적 견고성(soundness)과 완전성(completeness)]  #참고만

- 견고(sound) : {S = 공리들의 집합, L = 추론 규칙들의 집합}.

  : S로부터 L을 이용하여 유도될수 있는 모든 문장이 S의 논리적 귀결이면 추론 규칙 L은 논리적으로 견고하다.

- 완전(complete) : S의 논리적 귀결이 되는 모든 문장을 L을 이용하여 유도할수 있다면 추론 규칙 L은 논리적으로 완전하다.

[단일화(unification)] #예시 많이보기

: 두개의 서술식이 일치하도록 하기 위해 필요한 대체를 결정하는것.

: 추론과정을 수행하는데 필요한 작업. 결과를 내기위해 알맞은 식을 찾아 변수를 삽입하는 형태 

  => 여러 논리식 주어질때, 변수 이식해서 일치되는 식을 찾는것

ex) ∀X (man(X) => mortal(X)), man(socrates). {socrates/X}

   : man(socrates) => mortal(socrates) 도출