4-4. logic_Theorem proving, Resolution, Forward and Backward Chaining

Theorem proving

KB(우리가 알고있는 사실) 내 sentence들에 Inference rule(추론규칙)을 적용 -> 새로운 사실을 알아내는 것

Proof methods

Application to inference rules	Model checking
기존 문장 → 합리적인 새로운 문장 생성 inference rule application의 sequence를 통해 생성	n개의 model에 대한 Truth table 열거 model space에 대해 heuristic하게 search sound, incomplete

 

Resolution (분해)

Conjunctive Normal Form (CNF)

 

 

Forward chaining

• 기존 알려진 사실들을 기반으로 새로운 사실을 추리하며 나아가는 방법
• 한 문장에 대한 모든 전제가 알려져있는 사실이라면 그것에 대한 결론을 새로운 사실로써 KB에 추가
• 추가하는 과정을 통해 알고자 하는 사실 Q에 도달하거나, 더이상 추리가 불가능할때까지 반복

• soundness : 전건 긍정의 작용 -> 다 맞는말만 만들어짐
• completeness : KB에 entail되는 모든 atomic sentence를 derive
  • FC는 새로운 atomic sentence가 만들어지지 않는 fixed point에 도달
  • model m : 모든 symbol의 True/False를 부여한 final state
  • m은 KB의 model
  • KB를 entail하는 문장 q는 KB의 모든 model에서 True

Backward chaining

• 확인하고자 하는 사실 Q에서 backwards
• BC를 이용해 Q를 확인하는 방법
  • 1) Q가 이미 알려진 사실임을 확인
  • 2) KB 안에 있는 conclusion이 Q인 implication을 찾아냄
    • implication의 premise (전제)가 True인지 고민
    • implication이 알려져있다면 그걸 바탕으로 Q를 추론
    • 알려져있지 않다면 premise를 구성하는 symbol에 대해 또 다시 BC 하면서 T/F 여부 판단
    • 원래 알고있던 사실에 도달했을 때 위 반복을 멈추게 됨

Forward Chaining vs Backward Chaining

Forward Chaining	Backward Chaining
data-driven, automatic, unconscious 기존 사실 기반으로 과정 시작 goal과 무관한 work 많이 할 수 있음	goal-driven 확인하고자 하는 목표부터 과정 시작 cost 적은