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 기존 알려진 사실들을 기반으로 새로운 사실을 추리하며 나아가는 방법 ..