안녕하세요.이번에는 분해(resolution) 증명에 대해서 알아보도록 하겠습니다.분해 증명에 대해 이해 하기 위해, 분해(resolution), 논리곱 표준형(CNF: Conjunctive Normal Form), 분해 알고리즘에 대해서 함께 알아보겠습니다.1. 분해(Resolution) 우리는 앞의 포스팅들에서 증명을 이끌어 내는데 사용할 수 있는 추리규칙에 대해서 알아보았습니다. 그러한 추리규칙들이 건전하다. 올바르다라는 점을 함께 알아보았지만 아직 부족한 한가지는, 그러한 추리규칙들을 사용하는 추리 알고리즘이 완결적인지 알아보지 않았습니다. 여기서 완결적이라는 것은, 해당 알고리즘이 도달 가능한 목표가 존재할 때, 그것을 반드시 찾아낼수 있는가에 대한 것입니다. 따라서 이번에는 분해(Resolut..
