정리 증명
적어 둔 명제에서 새 명제를 어떻게 끌어낼까?
정리 증명
아는 것에서 새 참을 끌어냅니다
명제를 적는 까닭 가운데 하나는, 이미 아는 공리와 정리에서 새 정리를 추론하는 것입니다. 이 일을 컴퓨터가 하게 하는 것이 논리 프로그래밍의 바탕입니다.
공리(axiom)는 증명 없이 참으로 두는 명제이고, 정리(theorem)는 증명된 명제입니다. ⊂는 3편에서 본 함의로, 오른쪽이 참이면 왼쪽도 참입니다.
해결
같은 명제를 지우고 남은 것을 합칩니다
해결(resolution)은 주어진 명제들에서 새 명제를 끌어내는 추론 원리입니다. 한 절의 왼쪽과 다른 절의 오른쪽에 같은 명제가 있으면 둘을 지우고, 남은 것을 합쳐 새 절을 만듭니다.
절은 3편의 절 형식으로 적은 명제 하나입니다. 절 2는 예시입니다. ancestor(bill, jake)는 'bill은 jake의 조상이다'라는 뜻입니다.
단일화와 인스턴스화
변수 자리에 값을 끼워 맞춥니다
단일화(unification)는 두 명제가 같은 모양이 되도록 변수에 넣을 값을 찾는 일입니다. 변수에 값을 임시로 넣는 것을 인스턴스화(instantiation)라고 합니다.
father(X, mike)는 이 강의가 따르는 교재의 예로, 'mike의 아버지 X는 누구인가'입니다. 사실은 예시입니다. 점선 칸은 아직 값이 없는 변수입니다.
실패하면
값을 풀고 다른 값으로 다시
값을 넣었는데 나머지가 맞지 않으면 실패입니다. 그러면 넣은 값을 풀고 다른 값으로 다시 맞춰 봅니다. 이렇게 되돌아가는 것을 백트래킹(backtracking)이라고 합니다.
7편에서 자세히 봅니다. 사실 1은 교재의 예이고 사실 2는 예시입니다.
혼 절
왼쪽에 하나만, 또는 조건 없이 하나만
해결에는 제한된 모양의 명제인 혼 절(Horn clause)만 씁니다. ⊂ 왼쪽(머리)에 원자 명제가 하나만 있거나, ⊂ 없이 원자 명제 하나만 적은 것입니다. 대부분의 명제는 혼 절로 적을 수 있습니다.
머리(head)는 ⊂ 왼쪽의 결론 자리입니다. 머리 있는, 머리 없는이라는 이름은 교재를 따랐습니다.
선언적 의미론
문장 하나만 봐도 뜻이 정해집니다
명령형 언어의 문장은 앞에서 변수가 어떻게 바뀌었는지 따라가야 뜻을 압니다. 논리 프로그래밍의 문장은 그 문장만으로 뜻이 정해집니다. 이것이 선언적 의미론(declarative semantics)입니다.
의미론은 2강에서 본, 문장의 뜻을 정하는 것입니다. C는 1강에서 본 명령형 언어이고, 코드는 예시입니다.
다음 편