Model Checking, Logical Inference, Theorem Proving

 

A Simple Inference Example

- [1,2] 를 안전하게 방문할 수 있을까? -> [1,2] 에는 함정이 없을까? (간단한 예제이므로 괴물은 배제하고 생각함)

- In propositional logic

• Is ㄱP1,2 true? (1,2 에는 함정이 없나?)
• KB |= ㄱP1,2? (KB 에 의해 ㄱP1,2 가 entail 될 수 있나?)

- KB

- KB 는 다섯개의 sentence 의 집합이거나, 다섯개의 conjuncts를 가지고 있는 하나의 sentence 로 생각할 수 있다.

 

 

Inference by Model Checking

- M(KB) 는 M(ㄱP1,2) 에 포함되는지를 확인하는 것이 Model checking 이다.

- M(KB) 와 ㄱP1,2 에는 7개의 propositional symbol 이 존재한다. -> 2^7 개의 model 이 존재한다.

- 128 개의 모델 중 3개의 모델만 KB 값이 참이 된다.

- 따라서  3개의 모델에 대해서만 Model Checking 을 해보면 된다.

- 먼저, P1,2 의 진리값을 뒤집으면 ㄱP1,2 값이 되고, ㄱP1,2 는 3개의 모델에서 모두 true 값을 가진다.

- 즉, M(KB) 는 M(ㄱP1,2) 에 포함되는 것이 맞는 것을 알게 되었다. 

-> KB |= ㄱP1,2 는 Yes 이다.

 

 

 

Properties of Model Checking

- Sound?

• Yes. Model Checking은 logical entailment 의 정의를 그대로 구현하고 있기 때문이다. 
• 즉, KB |= a 는 M(KB) ⊆ M(a) 이므로, 답이 틀리지 않다.

- Complete?

• Yes. Model Checking 은 진리표를 만들어서 검사하는데, 진리표의 행은 유한하다. 
• 왜냐하면, propositional logic 에 존재하는 propositional symbol (n) 은 유한하기 때문이다. -> 검사도 2^n 으로 유한하다.

- Complexities?

• n : propositional symbol 의 개수
• 공간 복잡도는 O(n) 으로 좋다.
• 그러나 시간 복잡도는 한 행 한 행 모두 검사해야 하기 때문에 O(2^n) 으로 실용적이지 않다.

- 사실, propositional entailnent 는 co-NP-complete 문제이다. (NP complete 와 어려움의 정도가 같다.) 

 

 

 

Logical Equivalence

-> 즉, 두 sentence 가 같다는 것으로, a가 참이면 B도 참이고, a가 거짓일때는 B도 거짓이다.

 

Some Concepts

- Validity

• 모든 모델에서 true 인 sentence 를 valid 하다고 한다.
• ex) P v ㄱP -> 항상 true

- deduction theorem

• a |= B 는 a => B 가 valid 하다는 것과 같다.

- Satisfiability

• sentence 는 어떤 모델에서 참이된다면 satisfiable 하다고 한다.
• 즉, satisfable 하지 않은 sentence 는, 한 개의 모델에서도 참이 아니라는 것이다.
• 예)
• SAT 문제는 입력으로 하나의 sentence 가 주어지고, 이 문장이 satisfiable 한지를 답으로 내는 문제이다. 
  • 이 문제는 NP-complete 함이 증명되었다.

- Proof by refutation (모순에 의한 증명)

 

 

Theorem Proving for Logical Inference

- 모든 모델에 대해 M(KB) 가 M(a) 에 포함되는지를 확인하기 위해 열거하는 것 대신, inference rule 을 적용해서 결론을 도출해낼 수 있다.

- inference rule

• Modus Ponens
• 위에 있는 값이 둘다 모두 참이라면, B도 참이다.

• 

   
• And-Elimination
• 위에 있는 값이 참이라면, a도 참이다.

• 

• Logical equivalences
• 논리동치로, 위 아래를 바꿔도 성립한다. (modus ponens 와 and-elimination 은 위 아래를 바꿀 수 없다,)
• 예) biconditional elimination

• 

Theorem Proving Example

-> R2 에 biconditional elimination 을 적용하면 R6을 만들어낼 수 있다.

-> R6에  And-elimination 을 적용하면 R7 을 만들어낼 수 있다. 

-> R7 에 대우를 적용하면 R8 을 만들어낼 수 있다.

-> R4 와 R8 에 modus ponent 를 적용하면 R9 을 만들어낼 수 있다.

-> R9 에 드모르간 법칙을 적용하여 R10 을 만들어낼 수 있다.

-> end-elimination 을 적용하여 R11 을 만들어낼 수 있다. (Goal sentence : KB |= ㄱP1,2? )

 

 

Theorem Proving as Search

- Problem definition

-> goal 을 찾는 것이 중요하고 path 는 중요하지 않다.