Resolution  

Resolution 은 1965년에 J. A. Robinson 에 의해 제안된 증명기술이다. 그는 "Resolution Principle (도출원리)" 을 발견하였으나, 실제로 이 이론이 빛을 보게 된 것은 Robert A. Kowalski 의 Horn 절 (Horn clause) 에 기초를 둔 논리프로그래밍 (Logic Programming) 때문이다. 도출원리는 다음과 같은 절 집합이 모순이라는 것을 유도해가는 이론이다.

예를 들면, A->B, B->C 및 A 라는 전제로부터 C 를 증명할 경우, A->B=~AVB 및 B->C=BVC 에서 B 와 ~B 가 소거되어 새로운 절 ~AVC 가 도출된다. 이 절을 Resolvent 라고 하고, 이것을 본래의 절 {~AVB, ~BVC, A, ~C} 를 더하면, ~AVC 애서 A 가 소거되어 C 가 남는다. 이 C 와 ~C 는 공절 (Emptry Clause) 이 되고, 처음에 더한 C 의 부정인 ~C 가 모순이다. 이와 같은 도출원리인 증명과정은 바로 PROLOG 의 실행 프로세스가 되었다.

term :

도출법 (Resolution)   증명 (Proof)   정리증명 (Theorem Proving)    논리프로그래밍 (Logic Programming)    Prolog

paper :

비교흡수 방법 (Resolution) : Elaine Rich

도출법 (Resolution) : 이재규 외 : 도출법 (resolution) 은 명제계산 이나 술어계산 에서 정리를 증명하기 위해 이용되는 추론 규칙 으로서, 논리구 (Literal) 의 OR 결합으로만 이루어진 절 (Clause) 이라고 하는 특별한 논리식의 집합에 적용된다. 도출법 과정은 두 개의 부모절로부터 새로운 절을 생성하는 추론 과정으로서 ....

비교흡수 (resolution)   비교흡수 부정 (resolution refutation) : 유석인 : 지식 표현인 잘 구성된 공식 (wff) 의 한 종류로 절 (clause) 이 있는데, 절이란 문자들의 논리합으로 구성된 wff 로 정의된다. 여기서 논할 비교흡수방법이란 이러한 절들에 적용되는 하나의 중요한 추론규칙이다........